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 Th19;
then B is_closed_on o ;
then A2: rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o ;
(((B #) * the Arity of S1) . o) /\ ((((OSMSubSort A) #) * the Arity of S1) . o) = (((OSMSubSort A) #) * the Arity of S1) . o by A1, Th26, 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:71;
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:70;
hence rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A2; :: thesis: verum