let G be Group; :: thesis: for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )
let H be Subgroup of G; :: thesis: ( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )
thus Index H = card (Left_Cosets H) ; :: thesis: Index H = card (Right_Cosets H)
Left_Cosets H, Right_Cosets H are_equipotent by Th166;
hence Index H = card (Right_Cosets H) by CARD_1:21; :: thesis: verum