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 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
(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 S : verum } ))
let S be non empty non void ManySortedSign ; :: 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
(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 S : verum } ))
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
(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 S : verum } ))
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
(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 S : verum } ))
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
(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 S : verum } ))
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 (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 S : verum } )) )
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: (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 S : 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 S : verum } ;
set SA' = { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ;
set FS = { ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ;
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 A1, Th26;
then
commute F in Funcs the carrier of S,(Funcs I,{ ((F . i') . s1) where s1 is SortSymbol of S, 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 & rng F' c= Funcs I,{ ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } )
by FUNCT_2:def 2;
(commute F) . s in rng F'
by A2, FUNCT_1:def 5;
then consider F2 being Function such that
A3:
( F2 = (commute F) . s & dom F2 = I & rng F2 c= { ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } )
by A2, 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 S : 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 S : 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 S : verum } )
then consider i' being
set such that A4:
(
i' in dom ((commute F) . s) &
x' = ((commute F) . s) . i' )
by FUNCT_1:def 5;
reconsider i1 =
i' as
Element of
I by A3, A4;
consider F' being
ManySortedFunction of
U1,
(A . i1) such that A5:
(
F' = F . i1 &
F' is_homomorphism U1,
A . i1 )
by A1;
A6:
x' = F' . s
by A1, A4, A5, Th26;
A7:
dom (F' . s) = the
Sorts of
U1 . s
by FUNCT_2:def 1;
the
Sorts of
(A . i1) . s c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum }
then
rng (F' . s) c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum }
by XBOOLE_1:1;
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 S : verum } )
by A6, A7, 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 S : verum } ))
by A3, FUNCT_2:def 2; :: thesis: verum