let N be e_net; ( 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 )
the entrance of N * ( the entrance of N \ (id the carrier of N)) = {}
by Def2;
then A1:
the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {}
by Th11;
the escape of N * ( the escape of N \ (id the carrier of N)) = {}
by Def2;
then A2:
the escape of N * ( the escape of N \ (id (dom the escape of N))) = {}
by Th11;
A3:
the escape of N * the escape of N = the escape of N
by Def1;
then A4:
rng the escape of N = rng (CL the escape of N)
by A2, SYSREL:31;
A5:
the entrance of N * the entrance of N = the entrance of N
by Def1;
then
rng the entrance of N = rng (CL the entrance of N)
by A1, SYSREL:31;
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 A5, A1, A3, A2, A4, Th12, SYSREL:31; verum