Added proof of the corollary
Formatting
Fixed notation