deffunc H1( 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 H1(s1 * s2) = H1(s1) * H1(s2)
proof
let s1, s2 be Element of S; :: thesis: H1(s1 * s2) = H1(s1) * H1(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 H1(s1 * s2) = H1(s1) * H1(s2) by A6, FUNCT_1:10; :: thesis: verum
end;
A10: H1( 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 H1( 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 = H1(s) from GROUP_10:sch 1(A10, A2);
 hence ex b1 being LeftOperation of S,(the_subsets_of_card (n,E)) st
for s being Element of S holds b1 . s = the_extension_of_left_translation_of (n,s,LO) ; :: thesis: verum