let M be Pnet; ( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} )
A1:
rng ((Flow M) | the carrier' of M) c= the carrier of M
by Th9;
A2:
rng (((Flow M) ~) | the carrier' of M) c= the carrier of M
by Th9;
A3:
rng ((Flow M) | the carrier of M) c= the carrier' of M
by Th9;
A4:
rng (((Flow M) ~) | the carrier of M) c= the carrier' of M
by Th9;
A5:
dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M)
by Th10;
A6:
dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M)
by Th10;
A7:
rng ((Flow M) | the carrier of M) misses dom (id the carrier of M)
by Th10;
A8:
rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M)
by Th10;
A9:
rng (id the carrier of M) misses dom ((Flow M) | the carrier' of M)
by Th10;
A10:
rng (id the carrier of M) misses dom (((Flow M) ~) | the carrier' of M)
by Th10;
A11:
rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M)
by Th10;
rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M)
by Th10;
hence
( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, RELAT_1:44, RELAT_1:51, RELAT_1:53, RELAT_1:58; verum