let M be Pnet; :: thesis: ( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) )
set R = (Flow M) | the carrier' of M;
set S = ((Flow M) ~) | the carrier' of M;
set T = id the carrier' of M;
set R1 = (Flow M) | the carrier of M;
set S1 = ((Flow M) ~) | the carrier of M;
set T1 = id the carrier of M;
A1: dom ((Flow M) | the carrier' of M) c= the carrier' of M by RELAT_1:87;
A2: rng ((Flow M) | the carrier' of M) c= the carrier of M by Th14;
A3: dom (((Flow M) ~) | the carrier' of M) c= the carrier' of M by RELAT_1:87;
A4: rng (((Flow M) ~) | the carrier' of M) c= the carrier of M by Th14;
A5: dom (id the carrier' of M) c= the carrier' of M by Th14;
A6: rng (id the carrier' of M) c= the carrier' of M by Th14;
A7: dom ((Flow M) | the carrier of M) c= the carrier of M by RELAT_1:87;
A8: rng ((Flow M) | the carrier of M) c= the carrier' of M by Th14;
A9: dom (((Flow M) ~) | the carrier of M) c= the carrier of M by RELAT_1:87;
A10: rng (((Flow M) ~) | the carrier of M) c= the carrier' of M by Th14;
A11: dom (id the carrier of M) c= the carrier of M by Th14;
A12: rng (id the carrier of M) c= the carrier of M by Th14;
the carrier of M misses the carrier' of M by NET_1:def 2;
hence ( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm1; :: thesis: verum