let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra over 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 over 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 over 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 Th17, 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:71;
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:70;
B is opers_closed by A1, Th13;
then B is_closed_on o ;
then rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o ;
hence rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A2; :: thesis: verum