set E = the carrier of S;
deffunc H₁( Element of S) -> Element of bool [:the carrier of S,the carrier of S:] = the_left_translation_of $1;
A1: for s1, s2 being Element of S holds H₁(s1 * s2) = H₁(s1) * H₁(s2)

proof

let s1, s2 be Element of S; :: thesis: H₁(s1 * s2) = H₁(s1) * H₁(s2)
set f12 = the_left_translation_of (s1 * s2);
set f1 = the_left_translation_of s1;
set f2 = the_left_translation_of s2;
A2: ( the_left_translation_of (s1 * s2) in Funcs the carrier of S,the carrier of S & the_left_translation_of s1 in Funcs the carrier of S,the carrier of S & the_left_translation_of s2 in Funcs the carrier of S,the carrier of S ) by FUNCT_2:12;
then A3: ex f being Function st
( the_left_translation_of s1 = f & dom f = the carrier of S & rng f c= the carrier of S ) by FUNCT_2:def 2;
A4: ex f being Function st
( the_left_translation_of s2 = f & dom f = the carrier of S & rng f c= the carrier of S ) by A2, FUNCT_2:def 2;
A5: ex f being Function st
( the_left_translation_of (s1 * s2) = f & dom f = the carrier of S & rng f c= the carrier of S ) by A2, FUNCT_2:def 2;

A6: now

let x be set ; :: thesis: ( ( x in dom (the_left_translation_of (s1 * s2)) implies ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) ) ) & ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) implies x in dom (the_left_translation_of (s1 * s2)) ) )

hereby :: thesis: ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) implies x in dom (the_left_translation_of (s1 * s2)) )

assume A7: x in dom (the_left_translation_of (s1 * s2)) ; :: thesis: ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) )
hence x in dom (the_left_translation_of s2) by A4; :: thesis: (the_left_translation_of s2) . x in dom (the_left_translation_of s1)
(the_left_translation_of s2) . x in rng (the_left_translation_of s2) by A4, A7, FUNCT_1:12;
hence (the_left_translation_of s2) . x in dom (the_left_translation_of s1) by A3; :: thesis: verum

end;

assume ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) ) ; :: thesis: x in dom (the_left_translation_of (s1 * s2))
hence x in dom (the_left_translation_of (s1 * s2)) by A5; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom (the_left_translation_of (s1 * s2)) implies (the_left_translation_of (s1 * s2)) . x = (the_left_translation_of s1) . ((the_left_translation_of s2) . x) )
assume A8: x in dom (the_left_translation_of (s1 * s2)) ; :: thesis: (the_left_translation_of (s1 * s2)) . x = (the_left_translation_of s1) . ((the_left_translation_of s2) . x)
then reconsider s1' = x as Element of S ;
(the_left_translation_of s2) . x in rng (the_left_translation_of s2) by A4, A8, FUNCT_1:12;
then reconsider s1'' = (the_left_translation_of s2) . x as Element of S ;
thus (the_left_translation_of (s1 * s2)) . x = (s1 * s2) * s1' by TOPGRP_1:def 1
.= s1 * (s2 * s1') by GROUP_1:def 4
.= s1 * s1'' by TOPGRP_1:def 1
.= (the_left_translation_of s1) . ((the_left_translation_of s2) . x) by TOPGRP_1:def 1 ; :: thesis: verum

end;

hence H₁(s1 * s2) = H₁(s1) * H₁(s2) by A6, FUNCT_1:20; :: thesis: verum

end;

A9: H₁( 1_ S) = id the carrier of S

proof

set f = the_left_translation_of (1_ S);
the_left_translation_of (1_ S) in Funcs the carrier of S,the carrier of S by FUNCT_2:12;
then A10: ex f' being Function st
( the_left_translation_of (1_ S) = f' & dom f' = the carrier of S & rng f' c= the carrier of S ) by FUNCT_2:def 2;

now

let x be set ; :: thesis: ( x in the carrier of S implies (the_left_translation_of (1_ S)) . x = x )
assume x in the carrier of S ; :: thesis: (the_left_translation_of (1_ S)) . x = x
then reconsider s1 = x as Element of S ;
(the_left_translation_of (1_ S)) . s1 = (1_ S) * s1 by TOPGRP_1:def 1;
hence (the_left_translation_of (1_ S)) . x = x by GROUP_1:def 5; :: thesis: verum

end;

hence H₁( 1_ S) = id the carrier of S by A10, FUNCT_1:34; :: thesis: verum

end;

ex T being LeftOperation of S,the carrier of S st
for s being Element of S holds T . s = H₁(s) from GROUP_10:sch 1(A9, A1);
hence ex b₁ being LeftOperation of S,the carrier of S st
for s being Element of S holds b₁ . s = the_left_translation_of s ; :: thesis: verum