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
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
let A be MSAlgebra-Family of I,S; :: thesis: for s being SortSymbol of
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
let s be SortSymbol of ; :: thesis: for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
let U1 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
let F be ManySortedFunction of I; :: thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ;
set SA' = { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ;
set FS = { ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ;
F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) by A1, Th26;
then commute F in Funcs the carrier of S,(Funcs I,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) by FUNCT_6:85;
then consider F' being Function such that
A2: ( F' = commute F & dom F' = the carrier of S ) and
A3: rng F' c= Funcs I,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } by FUNCT_2:def 2;
(commute F) . s in rng F' by A2, FUNCT_1:def 5;
then A4: ex F2 being Function st
( F2 = (commute F) . s & dom F2 = I & rng F2 c= { ((F . i') . s1) where s1 is SortSymbol of , i' 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )

proof

let x' be set ; :: according to TARSKI:def 3 :: thesis: ( not x' in rng ((commute F) . s) or x' in Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ) )
assume x' in rng ((commute F) . s) ; :: thesis: x' in Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )
then consider i' being set such that
A5: i' in dom ((commute F) . s) and
A6: x' = ((commute F) . s) . i' by FUNCT_1:def 5;
reconsider i1 = i' as Element of I by A4, A5;
consider F' being ManySortedFunction of ,U1 such that
A7: F' = F . i1 and
F' is_homomorphism U1,A . i1 by A1;
the Sorts of (A . i1) . s c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum }

proof

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

end;

then A9: ( dom (F' . s) = the Sorts of U1 . s & rng (F' . s) c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ) by FUNCT_2:def 1, XBOOLE_1:1;
x' = F' . s by A1, A6, A7, Th26;
hence x' in Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )) by A4, FUNCT_2:def 2; :: thesis: verum