deffunc H₁( Element of S) -> Element of bool [: the carrier of S, the carrier of S:] = the_left_translation_of $1;
set E = the carrier of S;
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;
the_left_translation_of s1 in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9;
then A2: 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;
the_left_translation_of s2 in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9;
then A3: 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 FUNCT_2:def 2;
the_left_translation_of (s1 * s2) in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9;
then A4: 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 FUNCT_2:def 2;

A5: now :: thesis: for x being object holds
( ( 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)) ) )

let x be object ; :: 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 A6: 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 A3; :: 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 A3, A6, FUNCT_1:3;
hence (the_left_translation_of s2) . x in dom (the_left_translation_of s1) by A2; :: thesis: verum

end;

assume that
A7: x in dom (the_left_translation_of s2) and
(the_left_translation_of s2) . x in dom (the_left_translation_of s1) ; :: thesis: x in dom (the_left_translation_of (s1 * s2))
thus x in dom (the_left_translation_of (s1 * s2)) by A4, A7; :: thesis: verum

end;

now :: thesis: for x being object st x in dom (the_left_translation_of (s1 * s2)) holds
(the_left_translation_of (s1 * s2)) . x = (the_left_translation_of s1) . ((the_left_translation_of s2) . x)

let x be object ; :: 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 s19 = x as Element of S ;
(the_left_translation_of s2) . x in rng (the_left_translation_of s2) by A3, A8, FUNCT_1:3;
then reconsider s199 = (the_left_translation_of s2) . x as Element of S ;
thus (the_left_translation_of (s1 * s2)) . x = (s1 * s2) * s19 by TOPGRP_1:def 1
.= s1 * (s2 * s19) by GROUP_1:def 3
.= s1 * s199 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 A5, FUNCT_1:10; :: thesis: verum

end;

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

proof

set f = the_left_translation_of (1_ S);

A10: now :: thesis: for x being object st x in the carrier of S holds
(the_left_translation_of (1_ S)) . x = x

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

end;

thus H₁( 1_ S) = id the carrier of S by A10; :: 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