let n, m be Element of NAT ; :: thesis: ( n < m implies (disjointify f) . n misses (disjointify f) . m )
assume n < m ; :: thesis: (disjointify f) . n misses (disjointify f) . m
then A1: n in Segm m by NAT_1:44;
dom f = NAT by FUNCT_2:def 1;
then dom (f | m) = m /\ NAT by RELAT_1:61;
then n in dom (f | m) by A1, XBOOLE_0:def 4;
then A2: (f | m) . n in rng (f | m) by FUNCT_1:def 3;
(f | m) . n = f . n by A1, FUNCT_1:49;
then f . n misses (f . m) \ (union (rng (f | m))) by A2, XBOOLE_1:85, ZFMISC_1:74;
then A3: f . n misses (disjointify f) . m by Th4;
(f . n) \ (union (rng (f | n))) c= f . n by XBOOLE_1:36;
then (disjointify f) . n c= f . n by Th4;
hence (disjointify f) . n misses (disjointify f) . m by A3, XBOOLE_1:63; :: thesis: verum