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

per cases ( (B * the ResultSort of S) . o = {} or (B * the ResultSort of S) . o <> {} ) ;

suppose (B * the ResultSort of S) . o = {} ; :: thesis: B is_closed_on o

then A3: Result o,U0 = {} by A1, MSUALG_1:def 10;
Den o,U0 = {} by A3;
then rng ((Den o,U0) | (((B # ) * the Arity of S) . o)) = {} ;
hence rng ((Den o,U0) | (((B # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by XBOOLE_1:2; :: according to MSUALG_2:def 6 :: thesis: verum

end;

suppose (B * the ResultSort of S) . o <> {} ; :: thesis: B is_closed_on o

then Result o,U0 <> {} by A1, MSUALG_1:def 10;
then A4: ( dom (Den o,U0) = Args o,U0 & rng (Den o,U0) c= Result o,U0 ) by FUNCT_2:def 1, RELAT_1:def 19;
A5: Args o,U0 = ((B # ) * the Arity of S) . o by A1, MSUALG_1:def 9;
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 A4, A5, RELAT_1:97; :: according to MSUALG_2:def 6 :: thesis: verum

end;

end;

end;

let o be OperSymbol of S; :: thesis: o /. B = Den o,U0
B is_closed_on o by A2, Def7;
then A6: 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 A7: Result o,U0 = {} by A1, MSUALG_1:def 10;
Den o,U0 = {} by A7;
hence o /. B = Den o,U0 by A6; :: 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 A8: ( dom (Den o,U0) = Args o,U0 & rng (Den o,U0) c= Result o,U0 ) by FUNCT_2:def 1, RELAT_1:def 19;
Args o,U0 = ((B # ) * the Arity of S) . o by A1, MSUALG_1:def 9;
hence o /. B = Den o,U0 by A6, A8, RELAT_1:97; :: thesis: verum

end;

end;