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 H1( 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 = H1(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:62;
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 object ; :: 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 object such that
A5: y in dom (f | the carrier of H) and
A6: (f | the carrier of H) . y = x by FUNCT_1:def 3;
reconsider y = y as Element of H by A2, A5, RELAT_1:62;
reconsider y = y as Element of G by GROUP_2:42;
A7: f . y = (f | the carrier of H) . y by A5, FUNCT_1:47;
f . y = y |^ a by A1;
then x in (carr H) |^ a by A6, A7, Th41;
hence x in the carrier of (H |^ a) by Def6; :: thesis: verum
end;
let x be object ; :: 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
A8: x = b |^ a and
A9: b in carr H by Th41;
A10: f . b = b |^ a by A1;
(f | the carrier of H) . b = f . b by A3, A9, FUNCT_1:47;
hence x in rng (f | the carrier of H) by A3, A8, A9, A10, FUNCT_1:def 3; :: thesis: verum
end;
f | the carrier of H is one-to-one
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: 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
A11: x in dom (f | the carrier of H) and
A12: y in dom (f | the carrier of H) and
A13: (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, A11, A12, RELAT_1:62;
reconsider b = b, c = c as Element of G by GROUP_2:42;
A14: ( f . x = b |^ a & f . y = c |^ a ) by A1;
f . x = (f | the carrier of H) . x by A11, FUNCT_1:47;
hence x = y by A12, A13, A14, Th16, FUNCT_1:47; :: 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:5; :: thesis: verum