let I be non trivial finite set ; :: thesis: for CPNT being Colored-PT-net-Family of I holds not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty
let CPNT be Colored-PT-net-Family of I; :: thesis: not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty
deffunc H₁( Element of I, Element of I) -> FUNCTION_DOMAIN of Outbds (CPNT . $1), the carrier of (CPNT . $2) = Funcs ((Outbds (CPNT . $1)), the carrier of (CPNT . $2));
consider i0, j0 being Element of I such that
I0J0: i0 <> j0 by LMXorDelta;
set O12 = the Function of (Outbds (CPNT . i0)), the carrier of (CPNT . j0);
H₁(i0,j0) in { H₁(i,j) where i, j is Element of I : i <> j } by I0J0;
then H₁(i0,j0) c= union { H₁(i,j) where i, j is Element of I : i <> j } by ZFMISC_1:74;
hence not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty ; :: thesis: verum