let f be one-to-one Function; :: thesis: for A, B being Subset of (dom f) st A misses B holds
rng (f | A) misses rng (f | B)
let A, B be Subset of (dom f); :: thesis: ( A misses B implies rng (f | A) misses rng (f | B) )
assume ASC0: A misses B ; :: thesis: rng (f | A) misses rng (f | B)
assume rng (f | A) meets rng (f | B) ; :: thesis: contradiction
then consider y being set such that
ASC1: ( y in rng (f | A) & y in rng (f | B) ) by XBOOLE_0:3;
consider xa being set such that
ASC2: ( xa in dom (f | A) & y = (f | A) . xa ) by ASC1, FUNCT_1:def 5;
consider xb being set such that
ASC3: ( xb in dom (f | B) & y = (f | B) . xb ) by ASC1, FUNCT_1:def 5;
ASC4: ( xa in dom f & xb in dom f ) by RELAT_1:86, ASC2, ASC3;
( y = f . xa & y = f . xb ) by ASC2, ASC3, FUNCT_1:70;
then ASC5: xa = xb by FUNCT_1:def 8, ASC4;
( dom (f | A) c= A & dom (f | B) c= B ) by RELAT_1:87;
then xa in A /\ B by XBOOLE_0:def 4, ASC5, ASC2, ASC3;
hence contradiction by ASC0, XBOOLE_0:4; :: thesis: verum