let N be e_net; :: thesis: ( ((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ) = (the escape of N \ (id the carrier of N)) ~ & ((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ) = (the entrance of N \ (id the carrier of N)) ~ )
A1: ((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ) = ((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ by RELAT_1:54
.= (the escape of N \ (id the carrier of N)) ~ by Th31 ;
((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ) = ((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ by RELAT_1:54
.= (the entrance of N \ (id the carrier of N)) ~ by Th31 ;
hence ( ((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ) = (the escape of N \ (id the carrier of N)) ~ & ((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ) = (the entrance of N \ (id the carrier of N)) ~ ) by A1; :: thesis: verum