let G be finite Group; :: thesis: for H being Subgroup of G holds card G = (card H) * (index H)

let H be Subgroup of G; :: thesis: card G = (card H) * (index H)

reconsider C = Left_Cosets H as finite set ;

( D = union C & card D = (card H) * (card C) ) by Lm5;

union (Left_Cosets H) = the carrier of G by Th137;

hence card G = (card H) * (index H) by A6, Def18; :: thesis: verum

let H be Subgroup of G; :: thesis: card G = (card H) * (index 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 ) ) )

then A6:
ex D being finite set st 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 A1, Def15;

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 A3, Def15;

hence X,Y are_equipotent by A2, Th128; :: thesis: X misses Y

thus X misses Y by A2, A4, A5, Th115; :: thesis: verum

end;( 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 A1, Def15;

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 A3, Def15;

hence X,Y are_equipotent by A2, Th128; :: thesis: X misses Y

thus X misses Y by A2, A4, A5, Th115; :: thesis: verum

( D = union C & card D = (card H) * (card C) ) by Lm5;

union (Left_Cosets H) = the carrier of G by Th137;

hence card G = (card H) * (index H) by A6, Def18; :: thesis: verum