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 set ; :: 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 by MSUALG_1:def 7;
A4: ( dom the ResultSort of S1 = the carrier' of S1 & rng the ResultSort of S1 c= the carrier of S1 ) by FUNCT_2:def 1, RELAT_1:def 19;
then ((OSMSubSort A) * the ResultSort of S1) . o = (OSMSubSort A) . (the_result_sort_of o) by A3, FUNCT_1:23
.= meet (OSSubSort A,(the_result_sort_of o)) by Def11 ;
then consider X being set such that
A5: ( X in OSSubSort A,(the_result_sort_of o) & not x in X ) by A2, SETFAM_1:def 1;
consider B being OSSubset of OU0 such that
A6: ( B in OSSubSort A & B . (the_result_sort_of o) = X ) by A5, Def10;
rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A6, Th32;
then x in (B * the ResultSort of S1) . o by A1;
hence contradiction by A3, A4, A5, A6, FUNCT_1:23; :: thesis: verum