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 6;
then A2: rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by MSUALG_2:def 5;
(((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: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, XBOOLE_1:1; :: thesis: verum