set EE = the_subsets_of_card n,E;
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;
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;
A3:
(
the_extension_of_left_translation_of n,
(s1 * s2),
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E) &
the_extension_of_left_translation_of n,
s1,
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E) &
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:12;
then A4:
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;
A5:
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 A3, FUNCT_2:def 2;
A6:
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 A3, FUNCT_2:def 2;
A7:
now let x be
set ;
:: 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 A8:
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 A5;
:: 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 A5, A8, FUNCT_1:12;
hence
(the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO)
by A4;
:: thesis: verum
end; assume
(
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) )
;
:: thesis: x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)hence
x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)
by A6;
:: thesis: verum end;
now let x be
set ;
:: 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 A5, A9, FUNCT_1:12;
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:159
.=
(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 A7, FUNCT_1:20;
:: 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;
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:12;
then A11:
ex
f' being
Function st
(
the_extension_of_left_translation_of n,
(1_ S),
LO = f' &
dom f' = the_subsets_of_card n,
E &
rng f' c= the_subsets_of_card n,
E )
by FUNCT_2:def 2;
now let x be
set ;
:: 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 = xthen reconsider X =
x as
Element of
the_subsets_of_card n,
E ;
A12:
(the_extension_of_left_translation_of n,(1_ S),LO) . X = (LO ^ (1_ S)) .: X
by A1, Def4;
not
the_subsets_of_card n,
E is
empty
by A1, Th2;
then
X in the_subsets_of_card n,
E
;
then consider X' being
Subset of
E such that A13:
(
X' = X &
card X' = n )
;
(the_extension_of_left_translation_of n,(1_ S),LO) . x =
(id E) .: X'
by A12, A13, Def1
.=
X'
by FUNCT_1:162
;
hence
(the_extension_of_left_translation_of n,(1_ S),LO) . x = x
by A13;
:: thesis: verum end;
hence
H1(
1_ S)
= id (the_subsets_of_card n,E)
by A11, FUNCT_1:34;
:: 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