deffunc H₁( Element of H) -> Function of (Left_Cosets P),(Left_Cosets P) = the_left_translation_of ($1,P);
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 ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9;
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:9;
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 :: thesis: for x being object st x in dom (the_left_translation_of ((h1 * h2),P)) holds
(the_left_translation_of ((h1 * h2),P)) . x = (the_left_translation_of (h1,P)) . ((the_left_translation_of (h2,P)) . x)

let x be object ; :: 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 Left_Cosets P ;
(the_left_translation_of (h2,P)) . x in rng (the_left_translation_of (h2,P)) by A3, A5, FUNCT_1:3;
then reconsider P199 = (the_left_translation_of (h2,P)) . x as Element of Left_Cosets P ;
consider P299 being Element of Left_Cosets P, A199, A299 being Subset of G, g99 being Element of G such that
A6: ( P299 = (the_left_translation_of (h1,P)) . P199 & A299 = g99 * A199 & A199 = P199 & A299 = P299 ) and
A7: g99 = h1 by Def8;
reconsider P1999 = x as Element of Left_Cosets P by A5;
consider P29 being Element of Left_Cosets P, A19, A29 being Subset of G, g9 being Element of G such that
A8: ( P29 = (the_left_translation_of (h2,P)) . P19 & A29 = g9 * A19 & A19 = P19 & A29 = P29 ) and
A9: g9 = h2 by Def8;
consider P2999 being Element of Left_Cosets P, A1999, A2999 being Subset of G, g999 being Element of G such that
A10: ( P2999 = (the_left_translation_of ((h1 * h2),P)) . P1999 & A2999 = g999 * A1999 & A1999 = P1999 & A2999 = P2999 ) and
A11: g999 = h1 * h2 by Def8;
g999 = g99 * g9 by A9, A7, A11, GROUP_2:43;
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:32; :: thesis: verum

end;

the_left_translation_of ((h1 * h2),P) in Funcs ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9;
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 :: thesis: for x being object holds
( ( 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)) ) )

let x be object ; :: 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:3;
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:10; :: thesis: verum

end;

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

proof

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

now :: thesis: for x being object st x in Left_Cosets P holds
(the_left_translation_of ((1_ H),P)) . x = x

let x be object ; :: 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 G ex g being Element of G 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:44;
hence (the_left_translation_of ((1_ H),P)) . x = x by GROUP_2:37; :: thesis: verum

end;

hence H₁( 1_ H) = id (Left_Cosets P) ; :: thesis: verum

end;

ex T being LeftOperation of H,(Left_Cosets P) st
for h being Element of H 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 H holds b₁ . h = the_left_translation_of (h,P) ; :: thesis: verum