let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) )

assume A1: B = the Sorts of U0 ; :: thesis: ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

thus A2: B is opers_closed :: thesis: for o being OperSymbol of S holds o /. B = Den (o,U0)

B is_closed_on o by A2;

then A3: o /. B = (Den (o,U0)) | (((B #) * the Arity of S) . o) by Def7;

for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) )

assume A1: B = the Sorts of U0 ; :: thesis: ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

thus A2: B is opers_closed :: thesis: for o being OperSymbol of S holds o /. B = Den (o,U0)

proof

let o be OperSymbol of S; :: thesis: o /. B = Den (o,U0)
let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: B is_closed_on o

Result (o,U0) = (B * the ResultSort of S) . o by A1, MSUALG_1:def 5;

hence rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by RELAT_1:def 19; :: according to MSUALG_2:def 5 :: thesis: verum

end;Result (o,U0) = (B * the ResultSort of S) . o by A1, MSUALG_1:def 5;

hence rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by RELAT_1:def 19; :: according to MSUALG_2:def 5 :: thesis: verum

B is_closed_on o by A2;

then A3: o /. B = (Den (o,U0)) | (((B #) * the Arity of S) . o) by Def7;