let I be non empty set ; 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; 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 ; 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; for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)
let o be OperSymbol of S; (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 )
by MCART_1:def 1, MCART_1:def 2;
A2:
ex U0 being MSAlgebra of S st
( U0 = A . i & (OPER A) . i = the Charact of U0 )
by Def18;
A3:
dom (uncurry (OPER A)) = [:I,the carrier' of S:]
by Th12;
then A4:
[i,o] in dom (uncurry (OPER A))
by ZFMISC_1:106;
[:I,the carrier' of S:] <> {}
by ZFMISC_1:113;
then 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 set st x in I holds
g . x = (uncurry (OPER A)) . x,o
by A3, FUNCT_5:39;
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 4
.=
Den o,(A . i)
by MSUALG_1:def 11
;
hence
(A ?. o) . i = Den o,(A . i)
by A5; verum