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
(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 } ))))
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
(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 } ))))
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
(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 } ))))
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
(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 } ))))
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
(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 } ))))
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 (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 } )))) )
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: (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 } ))))
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
set SA9 = { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ;
F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A1, Th25;
then commute F in Funcs ( the carrier of S,(Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by FUNCT_6:55;
then consider F9 being Function such that
A2: ( F9 = commute F & dom F9 = the carrier of S ) and
A3: rng F9 c= Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by FUNCT_2:def 2;
(commute F) . s in rng F9 by A2, FUNCT_1:def 3;
then A4: ex F2 being Function st
( F2 = (commute F) . s & dom F2 = I & rng F2 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A3, FUNCT_2:def 2;
rng ((commute F) . s) c= 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 } ))

proof

let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in rng ((commute F) . s) or x9 in 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 } )) )
assume x9 in rng ((commute F) . s) ; :: thesis: x9 in 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 } ))
then consider i9 being object such that
A5: i9 in dom ((commute F) . s) and
A6: x9 = ((commute F) . s) . i9 by FUNCT_1:def 3;
reconsider i1 = i9 as Element of I by A4, A5;
consider F9 being ManySortedFunction of U1,(A . i1) such that
A7: F9 = F . i1 and
F9 is_homomorphism U1,A . i1 by A1;
the Sorts of (A . i1) . s c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum }

proof

A8: the Sorts of (A . i1) . s in { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the Sorts of (A . i1) . s or y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )
assume y in the Sorts of (A . i1) . s ; :: thesis: y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum }
hence y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A8, TARSKI:def 4; :: thesis: verum

end;

then A9: ( dom (F9 . s) = the Sorts of U1 . s & rng (F9 . s) c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ) by FUNCT_2:def 1;
x9 = F9 . s by A1, A6, A7, Th25;
hence x9 in 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 A9, FUNCT_2:def 2; :: thesis: verum

end;

hence (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 A4, FUNCT_2:def 2; :: thesis: verum