let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let OU0 be OSAlgebra of S1; :: thesis: for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let o be OperSymbol of S1; :: thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
let A, B be OSSubset of OU0; :: thesis: ( B in OSSubSort A implies rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o )
set m = (((OSMSubSort A) # ) * the Arity of S1) . o;
set b = ((B # ) * the Arity of S1) . o;
set d = Den o,OU0;
assume A1: B in OSSubSort A ; :: thesis: rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
then B is opers_closed by Th24;
then B is_closed_on o by MSUALG_2:def 7;
then A2: rng ((Den o,OU0) | (((B # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by MSUALG_2:def 6;
(((B # ) * the Arity of S1) . o) /\ ((((OSMSubSort A) # ) * the Arity of S1) . o) = (((OSMSubSort A) # ) * the Arity of S1) . o by A1, Th31, XBOOLE_1:28;
then (Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o) = ((Den o,OU0) | (((B # ) * the Arity of S1) . o)) | ((((OSMSubSort A) # ) * the Arity of S1) . o) by RELAT_1:100;
then rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= rng ((Den o,OU0) | (((B # ) * the Arity of S1) . o)) by RELAT_1:99;
hence rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A2, XBOOLE_1:1; :: thesis: verum