let G be Group; :: thesis: Index ((1). G) = card G

deffunc H_{1}( object ) -> set = {$1};

consider f being Function such that

A1: dom f = the carrier of G and

A2: for x being object st x in the carrier of G holds

f . x = H_{1}(x)
from FUNCT_1:sch 3();

A3: rng f = Left_Cosets ((1). G)

hence Index ((1). G) = card G by CARD_1:5; :: thesis: verum

deffunc H

consider f being Function such that

A1: dom f = the carrier of G and

A2: for x being object st x in the carrier of G holds

f . x = H

A3: rng f = Left_Cosets ((1). G)

proof

f is one-to-one
thus
rng f c= Left_Cosets ((1). G)
:: according to XBOOLE_0:def 10 :: thesis: Left_Cosets ((1). G) c= rng f

assume x in Left_Cosets ((1). G) ; :: thesis: x in rng f

then x in { {a} where a is Element of G : verum } by Th138;

then consider a being Element of G such that

A6: x = {a} ;

f . a = {a} by A2;

hence x in rng f by A1, A6, FUNCT_1:def 3; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets ((1). G) or x in rng f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Left_Cosets ((1). G) )

assume x in rng f ; :: thesis: x in Left_Cosets ((1). G)

then consider y being object such that

A4: y in dom f and

A5: f . y = x by FUNCT_1:def 3;

reconsider y = y as Element of G by A1, A4;

x = {y} by A2, A5;

then x in { {a} where a is Element of G : verum } ;

hence x in Left_Cosets ((1). G) by Th138; :: thesis: verum

end;assume x in rng f ; :: thesis: x in Left_Cosets ((1). G)

then consider y being object such that

A4: y in dom f and

A5: f . y = x by FUNCT_1:def 3;

reconsider y = y as Element of G by A1, A4;

x = {y} by A2, A5;

then x in { {a} where a is Element of G : verum } ;

hence x in Left_Cosets ((1). G) by Th138; :: thesis: verum

assume x in Left_Cosets ((1). G) ; :: thesis: x in rng f

then x in { {a} where a is Element of G : verum } by Th138;

then consider a being Element of G such that

A6: x = {a} ;

f . a = {a} by A2;

hence x in rng f by A1, A6, FUNCT_1:def 3; :: thesis: verum

proof

then
the carrier of G, Left_Cosets ((1). G) are_equipotent
by A1, A3, WELLORD2:def 4;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )

assume that

A7: ( x in dom f & y in dom f ) and

A8: f . x = f . y ; :: thesis: x = y

( f . y = {y} & f . x = {x} ) by A1, A2, A7;

hence x = y by A8, ZFMISC_1:3; :: thesis: verum

end;assume that

A7: ( x in dom f & y in dom f ) and

A8: f . x = f . y ; :: thesis: x = y

( f . y = {y} & f . x = {x} ) by A1, A2, A7;

hence x = y by A8, ZFMISC_1:3; :: thesis: verum

hence Index ((1). G) = card G by CARD_1:5; :: thesis: verum