let I be non empty set ; :: thesis: for i being Element of I
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)
let i be Element of I; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)
let o be OperSymbol of S; :: thesis: (A ?. o) . i = Den o,(A . i)
set O = the carrier' of S;
set f = uncurry (OPER A);
A2: [:I,the carrier' of S:] <> {} by ZFMISC_1:113;
A3: dom (uncurry (OPER A)) = [:I,the carrier' of S:] by Th12;
then consider g being Function such that
A4: ( (curry' (uncurry (OPER A))) . o = g & dom g = I & rng g c= rng (uncurry (OPER A)) & ( for x being set st x in I holds
g . x = (uncurry (OPER A)) . x,o ) ) by A2, FUNCT_5:39;
A5: [i,o] in dom (uncurry (OPER A)) by A3, ZFMISC_1:106;
A6: ( i in dom g & g . i = (uncurry (OPER A)) . i,o ) by A4;
A7: ( [i,o] `1 = i & [i,o] `2 = o ) by MCART_1:def 1, MCART_1:def 2;
ex U0 being MSAlgebra of S st
( U0 = A . i & (OPER A) . i = the Charact of U0 ) by Def18;
then g . i = the Charact of (A . i) . o by A5, A6, A7, FUNCT_5:def 4
.= Den o,(A . i) by MSUALG_1:def 11 ;
hence (A ?. o) . i = Den o,(A . i) by A4; :: thesis: verum