let G be addGroup; :: 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, DefA5;
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 Th42;
f . y = y * a by A1;
then x in (carr H) * a by A5, A6, Th41, FUNCT_1:47;
hence x in the carrier of (H * a) by Def6A; :: 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 Def6A;
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 Th42;
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, ThB16, FUNCT_1:47; :: thesis: verum

end;

hence card H = card (H * a) by A3, A4, WELLORD2:def 4, CARD_1:5; :: thesis: verum