let M be Pnet; :: thesis: ( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )
A1: (f_exit M) * (f_exit M) = f_exit M

proof

set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
A2: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th17;
A3: ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M by Th17;
A4: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:29;
(f_exit M) * (f_exit M) = (((Flow M) | 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))) by SYSREL:20
.= ((((Flow M) | the carrier' of M) * ((Flow M) | 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))) by RELAT_1:51
.= ((((Flow M) | the carrier' of M) * ((Flow M) | 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) * (id the carrier of M))) by RELAT_1:51
.= ({} \/ ((Flow M) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A2, A3, A4, Th16
.= f_exit M ;
hence (f_exit M) * (f_exit M) = f_exit M ; :: thesis: verum

end;

A5: (f_exit M) * (f_enter M) = f_exit M

proof

set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = ((Flow M) ~ ) | the carrier' of M;
A6: (id the carrier of M) * (((Flow M) ~ ) | the carrier' of M) = {} by Th17;
A7: ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M by Th17;
A8: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:29;
(f_exit M) * (f_enter M) = (((Flow M) | 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))) by SYSREL:20
.= ((((Flow M) | the carrier' of M) * (((Flow M) ~ ) | 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))) by RELAT_1:51
.= ((((Flow M) | the carrier' of M) * (((Flow M) ~ ) | 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) * (id the carrier of M))) by RELAT_1:51
.= ({} \/ ((Flow M) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A6, A7, A8, Th16
.= f_exit M ;
hence (f_exit M) * (f_enter M) = f_exit M ; :: thesis: verum

end;

A9: (f_enter M) * (f_enter M) = f_enter M

proof

set R = ((Flow M) ~ ) | the carrier' of M;
set S = id the carrier of M;
A10: (id the carrier of M) * (((Flow M) ~ ) | the carrier' of M) = {} by Th17;
A11: (((Flow M) ~ ) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~ ) | the carrier' of M by Th17;
A12: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:29;
(f_enter M) * (f_enter M) = ((((Flow M) ~ ) | 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))) by SYSREL:20
.= (((((Flow M) ~ ) | the carrier' of M) * (((Flow M) ~ ) | 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))) by RELAT_1:51
.= (((((Flow M) ~ ) | the carrier' of M) * (((Flow M) ~ ) | 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) * (id the carrier of M))) by RELAT_1:51
.= ({} \/ (((Flow M) ~ ) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A10, A11, A12, Th16
.= f_enter M ;
hence (f_enter M) * (f_enter M) = f_enter M ; :: thesis: verum

end;

(f_enter M) * (f_exit M) = f_enter M

proof

set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = ((Flow M) ~ ) | the carrier' of M;
A13: (((Flow M) ~ ) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~ ) | the carrier' of M by Th17;
A14: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th17;
A15: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:29;
(f_enter M) * (f_exit M) = ((((Flow M) ~ ) | 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))) by SYSREL:20
.= (((((Flow M) ~ ) | the carrier' of M) * ((Flow M) | 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))) by RELAT_1:51
.= (((((Flow M) ~ ) | the carrier' of M) * ((Flow M) | 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) * (id the carrier of M))) by RELAT_1:51
.= ({} \/ (((Flow M) ~ ) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A13, A14, A15, Th16
.= f_enter M ;
hence (f_enter M) * (f_exit M) = f_enter M ; :: thesis: verum

end;

hence ( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M ) by A1, A5, A9; :: thesis: verum