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);
A1: ( [i,o] `1 = i & [i,o] `2 = o ) ;
A2: ex U0 being MSAlgebra over S st
( U0 = A . i & (OPER A) . i = the Charact of U0 ) by Def11;
A3: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5;
then A4: [i,o] in dom (uncurry (OPER A)) by ZFMISC_1:87;
consider g being Function such that
A5: (curry' (uncurry (OPER A))) . o = g and
dom g = I and
rng g c= rng (uncurry (OPER A)) and
A6: for x being object st x in I holds
g . x = (uncurry (OPER A)) . (x,o) by A3, FUNCT_5:32, ZFMISC_1:90;
g . i = (uncurry (OPER A)) . (i,o) by A6;
then g . i = the Charact of (A . i) . o by A4, A1, A2, FUNCT_5:def 2
.= Den (o,(A . i)) by MSUALG_1:def 6 ;
hence (A ?. o) . i = Den (o,(A . i)) by A5; :: thesis: verum