let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds card H = card (H |^ a)
let a be Element of G; :: thesis: for H being Subgroup of G holds card H = card (H |^ a)
let H be Subgroup of G; :: thesis: card H = card (H |^ a)
deffunc H₁( Element of G) -> Element of G = $1 |^ a;
consider f being Function of the carrier of G,the carrier of G such that
A1: for g being Element of G holds f . g = H₁(g) from FUNCT_2:sch 4();
set g = f | the carrier of H;
A2: ( dom f = the carrier of G & the carrier of H c= the carrier of G ) by FUNCT_2:def 1, GROUP_2:def 5;
then A3: dom (f | the carrier of H) = the carrier of H by RELAT_1:91;
A4: rng (f | the carrier of H) = the carrier of (H |^ a)

proof

thus rng (f | the carrier of H) c= the carrier of (H |^ a) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (H |^ a) c= rng (f | the carrier of H)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f | the carrier of H) or x in the carrier of (H |^ a) )
assume x in rng (f | the carrier of H) ; :: thesis: x in the carrier of (H |^ a)
then consider y being set such that
A5: y in dom (f | the carrier of H) and
A6: (f | the carrier of H) . y = x by FUNCT_1:def 5;
reconsider y = y as Element of H by A2, A5, RELAT_1:91;
reconsider y = y as Element of G by GROUP_2:51;
( f . y = y |^ a & f . y = (f | the carrier of H) . y ) by A1, A5, FUNCT_1:70;
then x in (carr H) |^ a by A6, Th50;
hence x in the carrier of (H |^ a) by Def6; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (H |^ a) or x in rng (f | the carrier of H) )
assume x in the carrier of (H |^ a) ; :: thesis: x in rng (f | the carrier of H)
then x in (carr H) |^ a by Def6;
then consider b being Element of G such that
A7: x = b |^ a and
A8: b in carr H by Th50;
( (f | the carrier of H) . b = f . b & f . b = b |^ a ) by A1, A3, A8, FUNCT_1:70;
hence x in rng (f | the carrier of H) by A3, A7, A8, FUNCT_1:def 5; :: thesis: verum

end;

f | the carrier of H is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom (f | the carrier of H) or not b₁ in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom (f | the carrier of H) or not y in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . y or x = y )
assume that
A9: ( x in dom (f | the carrier of H) & y in dom (f | the carrier of H) ) and
A10: (f | the carrier of H) . x = (f | the carrier of H) . y ; :: thesis: x = y
reconsider b = x, c = y as Element of H by A2, A9, RELAT_1:91;
reconsider b = b, c = c as Element of G by GROUP_2:51;
( f . x = (f | the carrier of H) . x & f . y = (f | the carrier of H) . y & f . x = b |^ a & f . y = c |^ a ) by A1, A9, FUNCT_1:70;
hence x = y by A10, Th21; :: thesis: verum

end;

then the carrier of H,the carrier of (H |^ a) are_equipotent by A3, A4, WELLORD2:def 4;
hence card H = card (H |^ a) by CARD_1:21; :: thesis: verum