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 of S
for F being ManySortedFunction of 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 . i') . s1) where s1 is SortSymbol of S, 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 S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of 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 . i') . s1) where s1 is SortSymbol of S, 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 S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of 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 . i') . s1) where s1 is SortSymbol of S, 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 S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of 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 . i') . s1) where s1 is SortSymbol of S, i' 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 of S
for F being ManySortedFunction of 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 . i') . s1) where s1 is SortSymbol of S, 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 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 . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
let F be ManySortedFunction of ; :: 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 . i') . s1) where s1 is SortSymbol of S, 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,(A . i) 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 S, i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
set FS = { ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ;
set CA = the carrier of S;
A2: dom F = I by PARTFUN1:def 4;
A3: rng F c= Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of S, 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 S, 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 S, i' is Element of I : verum }
then consider i' being set such that
A4: ( i' in dom F & F . i' = x ) by FUNCT_1:def 5;
reconsider i1 = i' as Element of I by A4, PARTFUN1:def 4;
consider F' being ManySortedFunction of U1,(A . i1) such that
A5: ( F' = F . i1 & F' is_homomorphism U1,A . i1 ) by A1;
A6: dom F' = the carrier of S by PARTFUN1:def 4;
rng F' c= { ((F . i') . s1) where s1 is SortSymbol of S, 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 S, i' is Element of I : verum } )
assume x' in rng F' ; :: thesis: x' in { ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum }
then consider s' being set such that
A7: ( s' in dom F' & F' . s' = x' ) by FUNCT_1:def 5;
s' is SortSymbol of S by A7, PARTFUN1:def 4;
hence x' in { ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } by A5, A7; :: thesis: verum

end;

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

end;

then A8: F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ) by A2, FUNCT_2:def 2;
thus F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ) by A2, A3, FUNCT_2:def 2; :: thesis: ((commute F) . s) . i = (F . i) . s
thus ((commute F) . s) . i = (F . i) . s by A8, FUNCT_6:86; :: thesis: verum