let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let OU0 be OSAlgebra of S1; :: thesis: for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let o be OperSymbol of S1; :: thesis: for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let A be OSSubset of OU0; :: thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) or x in ((OSMSubSort A) * the ResultSort of S1) . o )
assume that
A1: x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) and
A2: not x in ((OSMSubSort A) * the ResultSort of S1) . o ; :: thesis: contradiction
set r = the_result_sort_of o;
A3: ( the_result_sort_of o = the ResultSort of S1 . o & dom the ResultSort of S1 = the carrier' of S1 ) by FUNCT_2:def 1, MSUALG_1:def 2;
then ((OSMSubSort A) * the ResultSort of S1) . o = (OSMSubSort A) . (the_result_sort_of o) by FUNCT_1:13
.= meet (OSSubSort (A,(the_result_sort_of o))) by Def11 ;
then consider X being set such that
A4: X in OSSubSort (A,(the_result_sort_of o)) and
A5: not x in X by A2, SETFAM_1:def 1;
consider B being OSSubset of OU0 such that
A6: B in OSSubSort A and
A7: B . (the_result_sort_of o) = X by A4, Def10;
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A6, Th27;
then x in (B * the ResultSort of S1) . o by A1;
hence contradiction by A3, A5, A7, FUNCT_1:13; :: thesis: verum