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)
proof
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;
let o be OperSymbol of S; :: thesis: 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;
per cases ( (B * the ResultSort of S) . o = {} or (B * the ResultSort of S) . o <> {} ) ;
suppose (B * the ResultSort of S) . o = {} ; :: thesis: o /. B = Den (o,U0)
then Result (o,U0) = {} by A1, MSUALG_1:def 5;
then Den (o,U0) = {} ;
hence o /. B = Den (o,U0) by A3; :: thesis: verum
end;
suppose (B * the ResultSort of S) . o <> {} ; :: thesis: o /. B = Den (o,U0)
Args (o,U0) = ((B #) * the Arity of S) . o by A1, MSUALG_1:def 4;
hence o /. B = Den (o,U0) by A3; :: thesis: verum
end;
end;