let x, y be object ; :: thesis: for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
let f, h be Function; :: thesis: ( (rng f) /\ (rng h) = {} & x in dom f & y in dom h implies f . x <> h . y )
assume A1: (rng f) /\ (rng h) = {} ; :: thesis: ( not x in dom f or not y in dom h or f . x <> h . y )
assume ( x in dom f & y in dom h ) ; :: thesis: f . x <> h . y
then ( f . x in rng f & h . y in rng h ) by FUNCT_1:def 3;
hence f . x <> h . y by A1, XBOOLE_0:def 4; :: thesis: verum