let f be one-to-one Function; 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); ( A misses B implies rng (f | A) misses rng (f | B) )
assume A1:
A misses B
; rng (f | A) misses rng (f | B)
assume
rng (f | A) meets rng (f | B)
; 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; verum