let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
(Den o,A) . x = (Den o,U0) . x
let U0 be MSAlgebra of S; :: thesis: for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
(Den o,A) . x = (Den o,U0) . x
let A be MSSubAlgebra of U0; :: thesis: for o being OperSymbol of S
for x being set st x in Args o,A holds
(Den o,A) . x = (Den o,U0) . x
let o be OperSymbol of S; :: thesis: for x being set st x in Args o,A holds
(Den o,A) . x = (Den o,U0) . x
let x be set ; :: thesis: ( x in Args o,A implies (Den o,A) . x = (Den o,U0) . x )
assume A1: x in Args o,A ; :: thesis: (Den o,A) . x = (Den o,U0) . x
reconsider B = the Sorts of A as MSSubset of U0 by MSUALG_2:def 10;
B is opers_closed by MSUALG_2:def 10;
then A2: B is_closed_on o by MSUALG_2:def 7;
thus (Den o,A) . x = ((Opers U0,B) . o) . x by MSUALG_2:def 10
.= (o /. B) . x by MSUALG_2:def 9
.= ((Den o,U0) | (((B # ) * the Arity of S) . o)) . x by A2, MSUALG_2:def 8
.= (Den o,U0) . x by A1, FUNCT_1:72 ; :: thesis: verum