deffunc H₁( Element of ) -> Function of Left_Cosets P, Left_Cosets P = the_left_translation_of $1,P;
A1: for h1, h2 being Element of holds H₁(h1 * h2) = H₁(h1) * H₁(h2)

proof

let h1, h2 be Element of ; :: 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 (Left_Cosets P),(Left_Cosets P) by FUNCT_2:12;
then A2: ex f being Function st
( the_left_translation_of h1,P = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) by FUNCT_2:def 2;
the_left_translation_of h2,P in Funcs (Left_Cosets P),(Left_Cosets P) by FUNCT_2:12;
then A3: ex f being Function st
( the_left_translation_of h2,P = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) 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 P1' = x as Element of Left_Cosets P ;
(the_left_translation_of h2,P) . x in rng (the_left_translation_of h2,P) by A3, A5, FUNCT_1:12;
then reconsider P1'' = (the_left_translation_of h2,P) . x as Element of Left_Cosets P ;
consider P2'' being Element of Left_Cosets P, A1'', A2'' being Subset of , g'' being Element of such that
A6: ( P2'' = (the_left_translation_of h1,P) . P1'' & A2'' = g'' * A1'' & A1'' = P1'' & A2'' = P2'' ) and
A7: g'' = h1 by Def8;
reconsider P1''' = x as Element of Left_Cosets P by A5;
consider P2' being Element of Left_Cosets P, A1', A2' being Subset of , g' being Element of such that
A8: ( P2' = (the_left_translation_of h2,P) . P1' & A2' = g' * A1' & A1' = P1' & A2' = P2' ) and
A9: g' = h2 by Def8;
consider P2''' being Element of Left_Cosets P, A1''', A2''' being Subset of , g''' being Element of such that
A10: ( P2''' = (the_left_translation_of (h1 * h2),P) . P1''' & A2''' = g''' * A1''' & A1''' = P1''' & A2''' = P2''' ) and
A11: g''' = h1 * h2 by Def8;
g''' = g'' * g' by A9, A7, A11, GROUP_2:52;
hence (the_left_translation_of (h1 * h2),P) . x = (the_left_translation_of h1,P) . ((the_left_translation_of h2,P) . x) by A8, A6, A10, GROUP_2:38; :: thesis: verum

end;

the_left_translation_of (h1 * h2),P in Funcs (Left_Cosets P),(Left_Cosets P) by FUNCT_2:12;
then A12: ex f being Function st
( the_left_translation_of (h1 * h2),P = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) 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 A13: 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, A13, 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
A14: 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 A12, A14; :: thesis: verum

end;

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

end;

A15: H₁( 1_ H) = id (Left_Cosets P)

proof

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

A16: now

let x be set ; :: thesis: ( x in Left_Cosets P implies (the_left_translation_of (1_ H),P) . x = x )
assume x in Left_Cosets P ; :: thesis: (the_left_translation_of (1_ H),P) . x = x
then reconsider P1 = x as Element of Left_Cosets P ;
( ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of ex g being Element of st
( P2 = (the_left_translation_of (1_ H),P) . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = 1_ H ) & 1_ H = 1_ G ) by Def8, GROUP_2:53;
hence (the_left_translation_of (1_ H),P) . x = x by GROUP_2:43; :: thesis: verum

end;

the_left_translation_of (1_ H),P in Funcs (Left_Cosets P),(Left_Cosets P) by FUNCT_2:12;
then ex f' being Function st
( the_left_translation_of (1_ H),P = f' & dom f' = Left_Cosets P & rng f' c= Left_Cosets P ) by FUNCT_2:def 2;
hence H₁( 1_ H) = id (Left_Cosets P) by A16, FUNCT_1:34; :: thesis: verum

end;

ex T being LeftOperation of H,(Left_Cosets P) st
for h being Element of holds T . h = H₁(h) from GROUP_10:sch 1(A15, A1);
hence ex b₁ being LeftOperation of H,(Left_Cosets P) st
for h being Element of holds b₁ . h = the_left_translation_of h,P ; :: thesis: verum