set O12 = the Function of (Outbds CPNT1), the carrier of CPNT2;
set O21 = the Function of (Outbds CPNT2), the carrier of CPNT1;
set Z = [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1];
take [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] ; :: thesis: ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] = [O12,O21]
thus ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] = [O12,O21] ; :: thesis: verum