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
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
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
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; :: thesis: ( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
set FS = { ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ;
set CA = the carrier of S;
A2: rng F c= Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum }

proof

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

proof

let x' be set ; :: according to TARSKI:def 3 :: thesis: ( not x' in rng F' or x' in { ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } )
assume x' in rng F' ; :: thesis: x' in { ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum }
then consider s' being set such that
A7: s' in dom F' and
A8: F' . s' = x' by FUNCT_1:def 5;
s' is SortSymbol of by A7, PARTFUN1:def 4;
hence x' in { ((F . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } by A5, A8; :: thesis: verum

end;

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

end;

A9: dom F = I by PARTFUN1:def 4;
hence F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of , i' 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 . i') . s1) where s1 is SortSymbol of , i' is Element of I : verum } ) by A9, A2, FUNCT_2:def 2;
hence ((commute F) . s) . i = (F . i) . s by FUNCT_6:86; :: thesis: verum