let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let A be MSAlgebra-Family of I,S; :: thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let s be SortSymbol of S; :: thesis: for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let U1 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
set SU = the Sorts of U1;
set SA = union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ;
let F be ManySortedFunction of ; :: thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s) )
assume A1:
for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i )
; :: thesis: for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
(commute F) . s in Funcs I,(Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ))
by A1, Th27;
then
commute ((commute F) . s) in Funcs (the Sorts of U1 . s),(Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ))
by FUNCT_6:85;
then consider f' being Function such that
A2:
f' = commute ((commute F) . s)
and
A3:
dom f' = the Sorts of U1 . s
and
A4:
rng f' c= Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } )
by FUNCT_2:def 2;
let x be set ; :: thesis: ( x in the Sorts of U1 . s implies (commute ((commute F) . s)) . x in product (Carrier A,s) )
assume A5:
x in the Sorts of U1 . s
; :: thesis: (commute ((commute F) . s)) . x in product (Carrier A,s)
f' . x in rng f'
by A5, A3, FUNCT_1:def 5;
then consider f being Function such that
A6:
f = (commute ((commute F) . s)) . x
and
A7:
dom f = I
and
rng f c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum }
by A2, A4, FUNCT_2:def 2;
A8:
now let i1 be
set ;
:: thesis: ( i1 in dom (Carrier A,s) implies ((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1 )assume
i1 in dom (Carrier A,s)
;
:: thesis: ((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1then reconsider i' =
i1 as
Element of
I by PARTFUN1:def 4;
consider F1 being
ManySortedFunction of
U1,
(A . i') such that A9:
F1 = F . i'
and
F1 is_homomorphism U1,
A . i'
by A1;
x in dom (F1 . s)
by A5, FUNCT_2:def 1;
then A10:
( ex
U0 being
MSAlgebra of
S st
(
U0 = A . i' &
(Carrier A,s) . i' = the
Sorts of
U0 . s ) &
(F1 . s) . x in rng (F1 . s) )
by FUNCT_1:def 5, PRALG_2:def 16;
f . i' = (F1 . s) . x
by A1, A5, A6, A9, Th28;
hence
((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1
by A6, A10;
:: thesis: verum end;
dom ((commute ((commute F) . s)) . x) = dom (Carrier A,s)
by A6, A7, PARTFUN1:def 4;
hence
(commute ((commute F) . s)) . x in product (Carrier A,s)
by A8, CARD_3:18; :: thesis: verum