let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of 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 of 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 7 :: thesis: B is_closed_on o
Result o,U0 = (B * the ResultSort of S) . o by A1, MSUALG_1:def 10;
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 6 :: thesis: verum

end;

let o be OperSymbol of S; :: thesis: o /. B = Den o,U0
B is_closed_on o by A2, Def7;
then A3: o /. B = (Den o,U0) | (((B # ) * the Arity of S) . o) by Def8;

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 10;
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

then Result o,U0 <> {} by A1, MSUALG_1:def 10;
then A4: dom (Den o,U0) = Args o,U0 by FUNCT_2:def 1;
Args o,U0 = ((B # ) * the Arity of S) . o by A1, MSUALG_1:def 9;
hence o /. B = Den o,U0 by A3, A4, RELAT_1:97; :: thesis: verum

end;

end;