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 over S
for F being ManySortedFunction of I 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 over S
for F being ManySortedFunction of I 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 over S
for F being ManySortedFunction of I 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 over S
for F being ManySortedFunction of I 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 over S; :: thesis: for F being ManySortedFunction of I 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 . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
let F be ManySortedFunction of I; :: 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 . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then commute ((commute F) . s) in Funcs (( the Sorts of U1 . s),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55;
then consider f9 being Function such that
A2: f9 = commute ((commute F) . s) and
A3: dom f9 = the Sorts of U1 . s and
A4: rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 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))
f9 . x in rng f9 by A5, A3, FUNCT_1:def 3;
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 . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A2, A4, FUNCT_2:def 2;

A8: now :: thesis: for i1 being object st i1 in dom (Carrier (A,s)) holds
((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1

let i1 be object ; :: 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)) . i1
then reconsider i9 = i1 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . i9) such that
A9: F1 = F . i9 and
F1 is_homomorphism U1,A . i9 by A1;
x in dom (F1 . s) by A5, FUNCT_2:def 1;
then A10: ( ex U0 being MSAlgebra over S st
( U0 = A . i9 & (Carrier (A,s)) . i9 = the Sorts of U0 . s ) & (F1 . s) . x in rng (F1 . s) ) by FUNCT_1:def 3, PRALG_2:def 9;
f . i9 = (F1 . s) . x by A1, A5, A6, A9, Th27;
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 2;
hence (commute ((commute F) . s)) . x in product (Carrier (A,s)) by A8, CARD_3:9; :: thesis: verum