let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
let o be OperSymbol of S; :: thesis: for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
let U0 be MSAlgebra of S; :: thesis: for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
let A, B be MSSubset of U0; :: thesis: ( B in SubSort A implies rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o )
set m = (((MSSubSort A) # ) * the Arity of S) . o;
set b = ((B # ) * the Arity of S) . o;
set d = Den o,U0;
assume A1: B in SubSort A ; :: thesis: rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
then (((B # ) * the Arity of S) . o) /\ ((((MSSubSort A) # ) * the Arity of S) . o) = (((MSSubSort A) # ) * the Arity of S) . o by Th18, XBOOLE_1:28;
then (Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o) = ((Den o,U0) | (((B # ) * the Arity of S) . o)) | ((((MSSubSort A) # ) * the Arity of S) . o) by RELAT_1:100;
then A2: rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= rng ((Den o,U0) | (((B # ) * the Arity of S) . o)) by RELAT_1:99;
B is opers_closed by A1, Th14;
then B is_closed_on o by Def7;
then rng ((Den o,U0) | (((B # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by Def6;
hence rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A2, XBOOLE_1:1; :: thesis: verum