let N be e_net; :: thesis: ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N )
A1: ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) )

proof

( the entrance of N * the entrance of N = the entrance of N & the entrance of N * (the entrance of N \ (id the carrier of N)) = {} ) by Def2, Def3;
then ( the entrance of N * the entrance of N = the entrance of N & the entrance of N * (the entrance of N \ (id (dom the entrance of N))) = {} ) by Th16;
hence ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) ) by SYSREL:50; :: thesis: verum

end;

( rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) )

proof

( the escape of N * the escape of N = the escape of N & the escape of N * (the escape of N \ (id the carrier of N)) = {} ) by Def2, Def3;
then ( the escape of N * the escape of N = the escape of N & the escape of N * (the escape of N \ (id (dom the escape of N))) = {} ) by Th16;
hence ( rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) ) by SYSREL:50; :: thesis: verum

end;

hence ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N ) by A1, Th17; :: thesis: verum