let G be Group; :: thesis: for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N
let N be normal Subgroup of G; :: thesis: ( Left_Cosets N is finite implies card (G ./. N) = index N )
assume Left_Cosets N is finite ; :: thesis: card (G ./. N) = index N
then reconsider LC = Left_Cosets N as finite set ;
thus card (G ./. N) = card LC
.= index N by GROUP_2:def 18 ; :: thesis: verum