let M be Pnet; :: thesis: ( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} )
A1: rng (the Flow of M | the Transitions of M) c= the Places of M by Th14;
A2: rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M by Th14;
A3: rng (the Flow of M | the Places of M) c= the Transitions of M by Th14;
A4: rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M by Th14;
A5: dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) by Th15;
A6: dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) by Th15;
A7: rng (the Flow of M | the Places of M) misses dom (id the Places of M) by Th15;
A8: rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) by Th15;
A9: rng (id the Places of M) misses dom (the Flow of M | the Transitions of M) by Th15;
A10: rng (id the Places of M) misses dom ((the Flow of M ~ ) | the Transitions of M) by Th15;
A11: rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) by Th15;
rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) by Th15;
hence ( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, RELAT_1:67, RELAT_1:77, RELAT_1:79, RELAT_1:87; :: thesis: verum