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 )

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; :: thesis: verum

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; :: thesis: verum