let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over 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 over 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 9;
B is opers_closed by MSUALG_2:def 9;
then A2: B is_closed_on o ;
thus (Den (o,A)) . x = ((Opers (U0,B)) . o) . x by MSUALG_2:def 9
.= (o /. B) . x by MSUALG_2:def 8
.= ((Den (o,U0)) | (((B #) * the Arity of S) . o)) . x by A2, MSUALG_2:def 7
.= (Den (o,U0)) . x by A1, FUNCT_1:49 ; :: thesis: verum