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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
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
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
set SU = the Sorts of U1;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
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 for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x )
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: for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
A2: (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then dom ((commute F) . s) = I by FUNCT_2:92;
then A3: ((commute F) . s) . i in rng ((commute F) . s) by FUNCT_1:def 3;
reconsider f9 = (commute F) . s as Function ;
rng ((commute F) . s) c= Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by A2, FUNCT_2:92;
then consider g being Function such that
A4: g = f9 . i and
dom g = the Sorts of U1 . s and
rng g c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A3, FUNCT_2:def 2;
let F9 be ManySortedFunction of U1,(A . i); :: thesis: ( F9 = F . i implies for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x )
assume A5: F9 = F . i ; :: thesis: for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
let x1 be set ; :: thesis: ( x1 in the Sorts of U1 . s implies for f being Function st f = (commute ((commute F) . s)) . x1 holds
f . i = (F9 . s) . x1 )
assume A6: x1 in the Sorts of U1 . s ; :: thesis: for f being Function st f = (commute ((commute F) . s)) . x1 holds
f . i = (F9 . s) . x1
let f be Function; :: thesis: ( f = (commute ((commute F) . s)) . x1 implies f . i = (F9 . s) . x1 )
assume A7: f = (commute ((commute F) . s)) . x1 ; :: thesis: f . i = (F9 . s) . x1
g = F9 . s by A1, A5, A4, Th25;
hence f . i = (F9 . s) . x1 by A6, A7, A2, A4, FUNCT_6:56; :: thesis: verum