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_{1}( 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_{1}(i0,j0) in { H_{1}(i,j) where i, j is Element of I : i <> j }
by I0J0;

then H_{1}(i0,j0) c= union { H_{1}(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

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

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

then H

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