let S be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; 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; verum