deffunc H₁( Element of S) -> Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) = the_extension_of_left_translation_of (n,$1,LO);
set EE = the_subsets_of_card (n,E);
A2: 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_extension_of_left_translation_of (n,(s1 * s2),LO);
set f1 = the_extension_of_left_translation_of (n,s1,LO);
set f2 = the_extension_of_left_translation_of (n,s2,LO);
the_extension_of_left_translation_of (n,s1,LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9;
then A3: ex f being Function st
( the_extension_of_left_translation_of (n,s1,LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def 2;
the_extension_of_left_translation_of (n,s2,LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9;
then A4: ex f being Function st
( the_extension_of_left_translation_of (n,s2,LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def 2;
the_extension_of_left_translation_of (n,(s1 * s2),LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9;
then A5: ex f being Function st
( the_extension_of_left_translation_of (n,(s1 * s2),LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def 2;

A6: now :: thesis: for x being object holds
( ( x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) implies ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ) ) & ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) implies x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ) )

let x be object ; :: thesis: ( ( x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) implies ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ) ) & ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) implies x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ) )

hereby :: thesis: ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) implies x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) )

assume A7: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ; :: thesis: ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) )
hence x in dom (the_extension_of_left_translation_of (n,s2,LO)) by A4; :: thesis: (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO))
(the_extension_of_left_translation_of (n,s2,LO)) . x in rng (the_extension_of_left_translation_of (n,s2,LO)) by A4, A7, FUNCT_1:3;
hence (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) by A3; :: thesis: verum

end;

assume that
A8: x in dom (the_extension_of_left_translation_of (n,s2,LO)) and
(the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ; :: thesis: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO))
thus x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) by A5, A8; :: thesis: verum

end;

now :: thesis: for x being object st x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) holds
(the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x)

let x be object ; :: thesis: ( x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) implies (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x) )
assume A9: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ; :: thesis: (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x)
then reconsider X1 = x as Element of the_subsets_of_card (n,E) ;
(the_extension_of_left_translation_of (n,s2,LO)) . x in rng (the_extension_of_left_translation_of (n,s2,LO)) by A4, A9, FUNCT_1:3;
then reconsider X2 = (the_extension_of_left_translation_of (n,s2,LO)) . x as Element of the_subsets_of_card (n,E) ;
thus (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (LO ^ (s1 * s2)) .: X1 by A1, Def4
.= ((LO ^ s1) * (LO ^ s2)) .: X1 by Def1
.= (LO ^ s1) .: ((LO ^ s2) .: X1) by RELAT_1:126
.= (LO ^ s1) .: X2 by A1, Def4
.= (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x) by A1, Def4 ; :: thesis: verum

end;

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

end;

A10: H₁( 1_ S) = id (the_subsets_of_card (n,E))

proof

set f = the_extension_of_left_translation_of (n,(1_ S),LO);

A11: now :: thesis: for x being object st x in the_subsets_of_card (n,E) holds
(the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x

let x be object ; :: thesis: ( x in the_subsets_of_card (n,E) implies (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x )
assume x in the_subsets_of_card (n,E) ; :: thesis: (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x
then reconsider X = x as Element of the_subsets_of_card (n,E) ;
not the_subsets_of_card (n,E) is empty by A1, Th1;
then X in the_subsets_of_card (n,E) ;
then consider X9 being Subset of E such that
A12: X9 = X and
card X9 = n ;
(the_extension_of_left_translation_of (n,(1_ S),LO)) . X = (LO ^ (1_ S)) .: X by A1, Def4;
then (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = (id E) .: X9 by A12, Def1
.= X9 by FUNCT_1:92 ;
hence (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x by A12; :: thesis: verum

end;

the_extension_of_left_translation_of (n,(1_ S),LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9;
then ex f9 being Function st
( the_extension_of_left_translation_of (n,(1_ S),LO) = f9 & dom f9 = the_subsets_of_card (n,E) & rng f9 c= the_subsets_of_card (n,E) ) by FUNCT_2:def 2;
hence H₁( 1_ S) = id (the_subsets_of_card (n,E)) by A11, FUNCT_1:17; :: thesis: verum

end;

ex T being LeftOperation of S,(the_subsets_of_card (n,E)) st
for s being Element of S holds T . s = H₁(s) from GROUP_10:sch 1(A10, A2);
hence ex b₁ being LeftOperation of S,(the_subsets_of_card (n,E)) st
for s being Element of S holds b₁ . s = the_extension_of_left_translation_of (n,s,LO) ; :: thesis: verum