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