let G be finite Group; :: thesis: for H being Subgroup of G holds card G = (card H) * ()
let H be Subgroup of G; :: thesis: card G = (card H) * ()
reconsider C = Left_Cosets H as finite set ;
now :: thesis: for X being set st X in C holds
ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )
let X be set ; :: thesis: ( X in C implies ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) ) )

assume A1: X in C ; :: thesis: ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )

then reconsider x = X as Subset of G ;
x is finite ;
then reconsider B = X as finite set ;
take B = B; :: thesis: ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )

thus B = X ; :: thesis: ( card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )

consider a being Element of G such that
A2: x = a * H by ;
ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C ) by Th133;
hence card B = card H by A2; :: thesis: for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y )

let Y be set ; :: thesis: ( Y in C & X <> Y implies ( X,Y are_equipotent & X misses Y ) )
assume that
A3: Y in C and
A4: X <> Y ; :: thesis: ( X,Y are_equipotent & X misses Y )
reconsider y = Y as Subset of G by A3;
A5: ex b being Element of G st y = b * H by ;
hence X,Y are_equipotent by ; :: thesis: X misses Y
thus X misses Y by A2, A4, A5, Th115; :: thesis: verum
end;
then A6: ex D being finite set st
( D = union C & card D = (card H) * (card C) ) by Lm5;
union () = the carrier of G by Th137;
hence card G = (card H) * () by ; :: thesis: verum