deffunc H₁( Element of H) -> Function of (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) = the_left_translation_of $1,p;
set E = the_sylow_p-subgroups_of_prime p,G;
A1: for h1, h2 being Element of H holds H₁(h1 * h2) = H₁(h1) * H₁(h2)

proof

let h1, h2 be Element of H; :: thesis: H₁(h1 * h2) = H₁(h1) * H₁(h2)
set f12 = the_left_translation_of (h1 * h2),p;
set f1 = the_left_translation_of h1,p;
set f2 = the_left_translation_of h2,p;
the_left_translation_of h1,p in Funcs (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) by FUNCT_2:12;
then A2: ex f being Function st
( the_left_translation_of h1,p = f & dom f = the_sylow_p-subgroups_of_prime p,G & rng f c= the_sylow_p-subgroups_of_prime p,G ) by FUNCT_2:def 2;
the_left_translation_of h2,p in Funcs (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) by FUNCT_2:12;
then A3: ex f being Function st
( the_left_translation_of h2,p = f & dom f = the_sylow_p-subgroups_of_prime p,G & rng f c= the_sylow_p-subgroups_of_prime p,G ) by FUNCT_2:def 2;

A4: now

let x be set ; :: thesis: ( x in dom (the_left_translation_of (h1 * h2),p) implies (the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x) )
assume A5: x in dom (the_left_translation_of (h1 * h2),p) ; :: thesis: (the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x)
then reconsider P19 = x as Element of the_sylow_p-subgroups_of_prime p,G ;
reconsider P1999 = x as Element of the_sylow_p-subgroups_of_prime p,G by A5;
consider P29 being Element of the_sylow_p-subgroups_of_prime p,G, H19, H29 being strict Subgroup of G, g2 being Element of G such that
A6: ( P29 = (the_left_translation_of h2,p) . P19 & P19 = H19 & P29 = H29 ) and
A7: h2 " = g2 and
A8: H29 = H19 |^ g2 by Def21;
(the_left_translation_of h2,p) . x in rng (the_left_translation_of h2,p) by A3, A5, FUNCT_1:12;
then reconsider P199 = (the_left_translation_of h2,p) . x as Element of the_sylow_p-subgroups_of_prime p,G ;
consider P299 being Element of the_sylow_p-subgroups_of_prime p,G, H199, H299 being strict Subgroup of G, g1 being Element of G such that
A9: P299 = (the_left_translation_of h1,p) . P199 and
A10: ( P199 = H199 & P299 = H299 ) and
A11: h1 " = g1 and
A12: H299 = H199 |^ g1 by Def21;
consider P2999 being Element of the_sylow_p-subgroups_of_prime p,G, H1999, H2999 being strict Subgroup of G, g3 being Element of G such that
A13: P2999 = (the_left_translation_of (h1 * h2),p) . P1999 and
A14: P1999 = H1999 and
A15: P2999 = H2999 and
A16: (h1 * h2) " = g3 and
A17: H2999 = H1999 |^ g3 by Def21;
g3 = (h2 " ) * (h1 " ) by A16, GROUP_1:25;
then P2999 = H1999 |^ (g2 * g1) by A7, A11, A15, A17, GROUP_2:52
.= P299 by A6, A8, A10, A12, A14, GROUP_3:72 ;
hence (the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x) by A9, A13; :: thesis: verum

end;

the_left_translation_of (h1 * h2),p in Funcs (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) by FUNCT_2:12;
then A18: ex f being Function st
( the_left_translation_of (h1 * h2),p = f & dom f = the_sylow_p-subgroups_of_prime p,G & rng f c= the_sylow_p-subgroups_of_prime p,G ) by FUNCT_2:def 2;

now

let x be set ; :: thesis: ( ( x in dom (the_left_translation_of (h1 * h2),p) implies ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) ) ) & ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) implies x in dom (the_left_translation_of (h1 * h2),p) ) )

hereby :: thesis: ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) implies x in dom (the_left_translation_of (h1 * h2),p) )

assume A19: x in dom (the_left_translation_of (h1 * h2),p) ; :: thesis: ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) )
hence x in dom (the_left_translation_of h2,p) by A3; :: thesis: (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p)
(the_left_translation_of h2,p) . x in rng (the_left_translation_of h2,p) by A3, A19, FUNCT_1:12;
hence (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) by A2; :: thesis: verum

end;

assume that
A20: x in dom (the_left_translation_of h2,p) and
(the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) ; :: thesis: x in dom (the_left_translation_of (h1 * h2),p)
thus x in dom (the_left_translation_of (h1 * h2),p) by A18, A20; :: thesis: verum

end;

hence H₁(h1 * h2) = H₁(h1) * H₁(h2) by A4, FUNCT_1:20; :: thesis: verum

end;

A21: H₁( 1_ H) = id (the_sylow_p-subgroups_of_prime p,G)

proof

set f = the_left_translation_of (1_ H),p;

A22: now

let x be set ; :: thesis: ( x in the_sylow_p-subgroups_of_prime p,G implies (the_left_translation_of (1_ H),p) . x = x )
assume x in the_sylow_p-subgroups_of_prime p,G ; :: thesis: (the_left_translation_of (1_ H),p) . x = x
then reconsider P1 = x as Element of the_sylow_p-subgroups_of_prime p,G ;
consider P2 being Element of the_sylow_p-subgroups_of_prime p,G, H1, H2 being strict Subgroup of G, g being Element of G such that
A23: ( P2 = (the_left_translation_of (1_ H),p) . P1 & P1 = H1 & P2 = H2 ) and
A24: (1_ H) " = g and
A25: H2 = H1 |^ g by Def21;
(1_ H) " = 1_ H by GROUP_1:16;
then g = 1_ G by A24, GROUP_2:53;
hence (the_left_translation_of (1_ H),p) . x = x by A23, A25, GROUP_3:73; :: thesis: verum

end;

the_left_translation_of (1_ H),p in Funcs (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) by FUNCT_2:12;
then ex f9 being Function st
( the_left_translation_of (1_ H),p = f9 & dom f9 = the_sylow_p-subgroups_of_prime p,G & rng f9 c= the_sylow_p-subgroups_of_prime p,G ) by FUNCT_2:def 2;
hence H₁( 1_ H) = id (the_sylow_p-subgroups_of_prime p,G) by A22, FUNCT_1:34; :: thesis: verum

end;

ex T being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of H holds T . h = H₁(h) from GROUP_10:sch 1(A21, A1);
hence ex b₁ being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of H holds b₁ . h = the_left_translation_of h,p ; :: thesis: verum