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)) | (((() #) * the Arity of S) . o)) c= (() * 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)) | (((() #) * the Arity of S) . o)) c= (() * the ResultSort of S) . o

let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 holds rng ((Den (o,U0)) | (((() #) * the Arity of S) . o)) c= (() * the ResultSort of S) . o
let A be MSSubset of U0; :: thesis: rng ((Den (o,U0)) | (((() #) * the Arity of S) . o)) c= (() * the ResultSort of S) . o
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((Den (o,U0)) | (((() #) * the Arity of S) . o)) or x in (() * the ResultSort of S) . o )
assume that
A1: x in rng ((Den (o,U0)) | (((() #) * the Arity of S) . o)) and
A2: not x in (() * 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 ;
then (() * the ResultSort of S) . o = () . by FUNCT_1:13
.= meet (SubSort (A,)) by Def14 ;
then consider X being set such that
A4: X in SubSort (A,) and
A5: not x in X by ;
consider B being MSSubset of U0 such that
A6: B in SubSort A and
A7: B . = X by ;
rng ((Den (o,U0)) | (((() #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by ;
then x in (B * the ResultSort of S) . o by A1;
hence contradiction by A3, A5, A7, FUNCT_1:13; :: thesis: verum