let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra over 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 over 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 over 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 object ; :: 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 & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 2;
then ((MSSubSort A) * the ResultSort of S) . o = (MSSubSort A) . (the_result_sort_of o) by FUNCT_1:13
.= meet (SubSort (A,(the_result_sort_of o))) by Def14 ;
then consider X being set such that
A4: X in SubSort (A,(the_result_sort_of o)) and
A5: not x in X by A2, SETFAM_1:def 1;
consider B being MSSubset of U0 such that
A6: B in SubSort A and
A7: B . (the_result_sort_of o) = X by A4, Def13;
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A6, Th18;
then x in (B * the ResultSort of S) . o by A1;
hence contradiction by A3, A5, A7, FUNCT_1:13; :: thesis: verum