let M be Pnet; :: thesis: ( ((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 ; :: thesis: verum