let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
let o be OperSymbol of S; :: thesis: for U0 being MSAlgebra of S
for A being MSSubset of U0 holds rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
let U0 be MSAlgebra of S; :: thesis: for A being MSSubset of U0 holds rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
let A be MSSubset of U0; :: thesis: rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) or x in ((MSSubSort A) * the ResultSort of S) . o )
assume that
A1: x in rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) and
A2: not x in ((MSSubSort A) * the ResultSort of S) . o ; :: thesis: contradiction
set r = the_result_sort_of o;
A3: the_result_sort_of o = the ResultSort of S . o by MSUALG_1:def 7;
A4: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1, RELAT_1:def 19;
((MSSubSort A) * the ResultSort of S) . o = (MSSubSort A) . (the_result_sort_of o) by A3, A4, FUNCT_1:23
.= meet (SubSort A,(the_result_sort_of o)) by Def15 ;
then consider X being set such that
A6: ( X in SubSort A,(the_result_sort_of o) & not x in X ) by A2, SETFAM_1:def 1;
consider B being MSSubset of U0 such that
A7: ( B in SubSort A & B . (the_result_sort_of o) = X ) by A6, Def14;
rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A7, Th19;
then x in (B * the ResultSort of S) . o by A1;
hence contradiction by A3, A4, A6, A7, FUNCT_1:23; :: thesis: verum