theorem Th15: :: FF_SIEC:15

for M being Pnet holds
( ((Flow M) | the carrier of M) ~ = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier' of M) ~ = ((Flow M) ~) | the carrier of M )