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 Def12;
defpred S₁[ set , set ] 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₂[ set , set ] 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 set st x in Outbds CPNT1 holds
ex y being set 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 set ; :: thesis: ( x in Outbds CPNT1 implies ex y being set 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 set 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};
consider y being Function of (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01));
take y ; :: thesis: ( 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] )
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:141;
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:128;
y in Funcs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) by FUNCT_2:11;
then y in PFuncs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) by A4;
hence ( 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] ) 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 set st x in Outbds CPNT1 holds
S₂[x,q12 . x] from FUNCT_2:sch 1(A2);

A8: now

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 set st x in Outbds CPNT2 holds
ex y being set 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 set ; :: thesis: ( x in Outbds CPNT2 implies ex y being set 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 set 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};
consider y being Function of (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02));
take y ; :: thesis: ( 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] )
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:141;
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:128;
y in Funcs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) by FUNCT_2:11;
then y in PFuncs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) by A11;
hence ( 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] ) 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 set st x in Outbds CPNT2 holds
S₁[x,q21 . x] from FUNCT_2:sch 1(A9);

A15: now

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