set L2 = bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2));
set L1 = bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2));
set K2 = bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1));
set K1 = bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1));
set TO2 = Outbds CPNT2;
set TO1 = Outbds CPNT1;
set Y1 = PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1))));
set Y2 = PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2))));
consider O12 being Function of (Outbds CPNT1), the carrier of CPNT2, O21 being Function of (Outbds CPNT2), the carrier of CPNT1 such that
A1: O = [O12,O21] by Def13;
defpred S₁[ object , object ] means ex t02 being transition of CPNT2 st
( $1 = t02 & $2 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) );
defpred S₂[ object , object ] means ex t01 being transition of CPNT1 st
( $1 = t01 & $2 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) );
A2: for x being object st x in Outbds CPNT1 holds
ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in Outbds CPNT1 implies ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S₂[x,y] ) )
assume x in Outbds CPNT1 ; :: thesis: ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S₂[x,y] )
then consider t01 being transition of CPNT1 such that
A3: x = t01 and
t01 is outbound ;
set t2 = Im (O12,t01);
set t1 = *' {t01};
set y = the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))));
take the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ; :: thesis: ( the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) in PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S₂[x, the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))] )
set H1 = thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}));
set H2 = thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)));
A4: Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) c= PFuncs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) by FUNCT_2:72;
A5: thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))) c= bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)) by Lm1;
thin_cylinders ( the ColoredSet of CPNT1,(*' {t01})) c= bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1)) by Lm1;
then A6: PFuncs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) c= PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) by A5, PARTFUN1:50;
the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) in Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) by FUNCT_2:8;
then the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) in PFuncs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) by A4;
hence ( the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) in PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S₂[x, the Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))] ) by A3, A6; :: thesis: verum

end;

consider q12 being Function of (Outbds CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1))))) such that
A7: for x being object st x in Outbds CPNT1 holds
S₂[x,q12 . x] from FUNCT_2:sch 1(A2);

A8: now :: thesis: for tt01 being transition of CPNT1 st tt01 is outbound holds
q12 . tt01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {tt01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,tt01))))

let tt01 be transition of CPNT1; :: thesis: ( tt01 is outbound implies q12 . tt01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {tt01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,tt01)))) )
assume tt01 is outbound ; :: thesis: q12 . tt01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {tt01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,tt01))))
then tt01 in Outbds CPNT1 ;
then ex t01 being transition of CPNT1 st
( tt01 = t01 & q12 . tt01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) by A7;
hence q12 . tt01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {tt01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,tt01)))) ; :: thesis: verum

end;

A9: for x being object st x in Outbds CPNT2 holds
ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Outbds CPNT2 implies ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) & S₁[x,y] ) )
assume x in Outbds CPNT2 ; :: thesis: ex y being object st
( y in PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) & S₁[x,y] )
then consider t02 being transition of CPNT2 such that
A10: x = t02 and
t02 is outbound ;
set t2 = Im (O21,t02);
set t1 = *' {t02};
set y = the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))));
take the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ; :: thesis: ( the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) in PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) & S₁[x, the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))] )
set H1 = thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}));
set H2 = thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)));
A11: Funcs ((thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))) c= PFuncs ((thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))) by FUNCT_2:72;
A12: thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))) c= bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)) by Lm1;
thin_cylinders ( the ColoredSet of CPNT2,(*' {t02})) c= bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2)) by Lm1;
then A13: PFuncs ((thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))) c= PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) by A12, PARTFUN1:50;
the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) in Funcs ((thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))) by FUNCT_2:8;
then the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) in PFuncs ((thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))) by A11;
hence ( the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) in PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2)))) & S₁[x, the Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02))))] ) by A10, A13; :: thesis: verum

end;

consider q21 being Function of (Outbds CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the ColoredSet of CPNT2))))) such that
A14: for x being object st x in Outbds CPNT2 holds
S₁[x,q21 . x] from FUNCT_2:sch 1(A9);

A15: now :: thesis: for tt02 being transition of CPNT2 st tt02 is outbound holds
q21 . tt02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {tt02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,tt02))))

let tt02 be transition of CPNT2; :: thesis: ( tt02 is outbound implies q21 . tt02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {tt02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,tt02)))) )
assume tt02 is outbound ; :: thesis: q21 . tt02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {tt02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,tt02))))
then tt02 in Outbds CPNT2 ;
then ex t02 being transition of CPNT2 st
( tt02 = t02 & q21 . tt02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) by A14;
hence q21 . tt02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {tt02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,tt02)))) ; :: thesis: verum

end;

take [q12,q21] ; :: thesis: ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) & [q12,q21] = [q12,q21] )
A16: dom q21 = Outbds CPNT2 by FUNCT_2:def 1;
dom q12 = Outbds CPNT1 by FUNCT_2:def 1;
hence ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) & [q12,q21] = [q12,q21] ) by A1, A8, A15, A16; :: thesis: verum