let I be non empty set ; 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 ; 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; 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; 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; 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; 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; ( ( 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 )
; ( 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 ;
TARSKI:def 3 ( 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
;
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 }
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;
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; ((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; verum