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 A1: 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 object such that
A2: ( y in rng (f | A) & y in rng (f | B) ) by XBOOLE_0:3;
consider xa being object such that
A3: ( xa in dom (f | A) & y = (f | A) . xa ) by A2, FUNCT_1:def 3;
consider xb being object such that
A4: ( xb in dom (f | B) & y = (f | B) . xb ) by A2, FUNCT_1:def 3;
A5: ( xa in dom f & xb in dom f ) by A3, A4, RELAT_1:57;
( y = f . xa & y = f . xb ) by A3, A4, FUNCT_1:47;
then A6: xa = xb by A5, FUNCT_1:def 4;
( dom (f | A) c= A & dom (f | B) c= B ) by RELAT_1:58;
then xa in A /\ B by A6, A3, A4, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:4; :: thesis: verum