let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for i being Element of I
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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let S be non empty non void ManySortedSign ; :: thesis: for i being Element of I
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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
let i be Element of I; :: 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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . 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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . 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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . 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
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
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 ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . 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: ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ;
set CA = the carrier of S;
A2: rng F c= Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) )
assume x in rng F ; :: thesis: x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )
then consider i9 being object such that
A3: i9 in dom F and
A4: F . i9 = x by FUNCT_1:def 3;
reconsider i1 = i9 as Element of I by A3;
consider F9 being ManySortedFunction of U1,(A . i1) such that
A5: F9 = F . i1 and
F9 is_homomorphism U1,A . i1 by A1;
A6: rng F9 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum }

proof

let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in rng F9 or x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } )
assume x9 in rng F9 ; :: thesis: x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum }
then consider s9 being object such that
A7: s9 in dom F9 and
A8: F9 . s9 = x9 by FUNCT_1:def 3;
s9 is SortSymbol of S by A7;
hence x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } by A5, A8; :: thesis: verum

end;

dom F9 = the carrier of S by PARTFUN1:def 2;
hence x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A4, A5, A6, FUNCT_2:def 2; :: thesis: verum

end;

A9: dom F = I by PARTFUN1:def 2;
hence 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 A2, FUNCT_2:def 2; :: thesis: ((commute F) . s) . i = (F . i) . s
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 A9, A2, FUNCT_2:def 2;
hence ((commute F) . s) . i = (F . i) . s by FUNCT_6:56; :: thesis: verum