:: Cell Petri Net Concepts
::  by Mitsuru Jitsukawa , Pauline N. Kawamoto , Yasunari Shidama and Yatsuka Nakamura
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies RELAT_1, NET_1, ARYTM_3, BOOLE, PETRI, PETRI_2, FUNCT_1, ARYTM,
      FINSET_1, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, SETFAM_1, COMPLEX1,
      REALSET1;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, SETFAM_1, RELAT_1,
      RELSET_1, DOMAIN_1, PETRI, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, RELSET_2,
      FINSET_1, FUNCOP_1, CARD_1, NUMBERS;
 constructors RELAT_1, ENUMSET1, RELSET_1, DOMAIN_1, MEMBERED, XBOOLE_0,
      VALUED_1, PETRI, FUNCT_2, PARTFUN1, RELSET_2, SEQ_1, FUNCOP_1, ORDINAL1,
      FINSET_1, NAT_1, FUNCT_4, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1,
      WELLORD2;
 registrations SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, PARTFUN1, RELSET_1,
      XBOOLE_0, MEMBERED, FUNCOP_1, TREES_2, VALUED_1, XXREAL_0, XREAL_0,
      REAL_1, ZFMISC_1, NAT_1, FUNCT_2, FUNCT_4, FINSET_1, PETRI, REALSET1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions ENUMSET1, TARSKI, XBOOLE_0, PETRI, FUNCT_2, FUNCT_4, PARTFUN1,
      ORDINAL1, FUNCOP_1, WELLORD2, RELAT_1, FINSET_1, RELSET_1, CARD_1;
 theorems RELSET_1, PARTFUN1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, PETRI,
      FUNCT_1, FUNCT_2, XBOOLE_1, FUNCT_4, FUNCOP_1, RELSET_2;
 schemes FUNCT_2;

begin :: Preliminaries: thin cylinder, locus

 reserve PTN for PT_net_Str;
 reserve y for Function;
 reserve z for set;

definition
  let A be non empty set, B be set;
  let Bo be set, yo be Function of Bo,A;
  assume
AS: Bo c= B;
  func cylinder0(A,B,Bo,yo) ->  non empty Subset of Funcs(B,A) equals
  :DefX01:
  { y where y is Function of B,A : y|Bo = yo };
  correctness
  proof
    set D = { y where y is Function of B,A : y|Bo = yo };
A3: now let z be set;
    assume z in D; then
    ex y be Function of B,A st z=y & y|Bo = yo;
    hence z in Funcs(B,A) by FUNCT_2:11;
  end;
  now per cases;
  suppose C1: Bo = {};
    consider f being Function of B,A;
    f|{} = {} .= yo by C1;
    then f in D by C1;
    hence D is non empty;
  end;
  suppose Bo <> {}; then
    consider b0 be set such that
D2: b0 in Bo by XBOOLE_0:def 1;
    set f = (B --> yo.b0) +* yo;
C:  rng f c= rng(B --> yo.b0) \/ rng yo by FUNCT_4:18;
E:  rng(B --> yo.b0) c= {yo.b0} by FUNCOP_1:19;
B:  dom yo = Bo by FUNCT_2:def 1;
    yo.b0 in A by D2,FUNCT_2:7;
    then {yo.b0} c= A by ZFMISC_1:37;
    then
D:  rng(B --> yo.b0) c= A by E,XBOOLE_1:1;
    rng yo c= A by RELSET_1:12;
    then
A:   rng(B --> yo.b0) \/ rng yo c= A by D,XBOOLE_1:8;
    dom f = dom(B --> yo.b0) \/ Bo by B,FUNCT_4:def 1
       .= B \/ Bo by FUNCOP_1:19
       .= B by AS,XBOOLE_1:12;
    then reconsider f as Function of B,A by A,FUNCT_2:4,C,XBOOLE_1:1;
    f|Bo = yo by B,FUNCT_4:24;
    then f in D;
    hence D is non empty;
    end;
  end;
  hence thesis by A3,TARSKI:def 3;
  end;
end;

definition
  let A be non empty set, B be set;
  mode thin_cylinder of A,B -> non empty Subset of Funcs(B,A) means
  :Def21:
  ex Bo being Subset of B,yo being Function of Bo,A st
  Bo is finite &
  it = cylinder0(A,B,Bo,yo);
  existence
  proof
    set Bo={};
A2: Bo is Subset of B & Bo is finite by XBOOLE_1:2;
    consider yo being Function of Bo,A;
    take D= cylinder0(A,B,Bo,yo);
    thus thesis by A2;
  end;
end;

theorem LM1:
  for A be non empty set, B be set,
  D be thin_cylinder of A,B holds
  ex Bo being Subset of B,yo being Function of Bo,A st
  Bo is finite &
  D = { y where y is Function of B,A : y|Bo = yo }
  proof
    let A be non empty set, B be set,
        D be thin_cylinder of A,B;
    consider Bo being Subset of B,yo being Function of Bo,A such that
A1: Bo is finite &
    D = cylinder0(A,B,Bo,yo) by Def21;
    D = { y where y is Function of B,A : y|Bo = yo } by DefX01,A1;
    hence thesis by A1;
  end;

theorem
  for A1,A2 be non empty set, B be set,
  D1 be thin_cylinder of A1,B st A1 c= A2
  ex D2 be thin_cylinder of A2,B st D1 c= D2
  proof
    let A1,A2 be non empty set, B be set,
    D1 be thin_cylinder of A1,B;
    assume AS: A1 c= A2;
    consider Bo being Subset of B,yo1 being Function of Bo,A1 such that
P1: Bo is finite &
    D1 = { y  where y is Function of B,A1: y|Bo = yo1 } by LM1;
    reconsider yo2=yo1 as Function of Bo,A2 by AS, FUNCT_2:9;
    set D2= { y  where y is Function of B,A2: y|Bo = yo2 };
S1: now let x be set;
    assume x in D1;
    then consider y1 be Function of B,A1 such that
P4: x=y1 & y1|Bo = yo1 by P1;
    reconsider y2=y1 as Function of B,A2 by FUNCT_2:9,AS;
    x=y1 & y2|Bo = yo1 by P4;
    hence x in D2;
  end;
  D2= cylinder0(A2,B,Bo,yo2) by DefX01;
  then reconsider D2 as thin_cylinder of A2,B by P1,Def21;
  take D2;
  thus thesis by S1,TARSKI:def 3;
end;

definition
  let A be non empty set, B be set;
  func thin_cylinders(A,B) -> non empty Subset-Family of Funcs(B,A)
  equals
  {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
  correctness
  proof
    consider F be thin_cylinder of A,B;
P2: F in {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
    now let z be set;
    assume
    z in {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
    then ex D be Subset of Funcs(B,A) st
    z=D & D is thin_cylinder of A,B;
    hence z in bool Funcs(B,A);
  end;
  hence thesis by P2,TARSKI:def 3;
  end;
end;

LmThin:
  for A be non empty set, B,C be set st B c= C
  holds thin_cylinders(A,B) c= bool PFuncs(C,A)
  proof
    let A be non empty set, B,C be set;
    assume AS: B c= C;
    let x be set;
    assume x in thin_cylinders(A,B);
    then consider D be Subset of Funcs(B,A) such that
P1: x=D & D is thin_cylinder of A,B;
P2: D in bool Funcs(B,A);
P3: Funcs(B,A) c= PFuncs(B,A) by FUNCT_2:141;
    PFuncs(B,A) c= PFuncs(C,A) by AS,PARTFUN1:128;
    then
    Funcs(B,A) c= PFuncs(C,A) by XBOOLE_1:1,P3;
    then
    bool Funcs(B,A) c= bool PFuncs(C,A) by ZFMISC_1:79;
    hence x in bool PFuncs(C,A) by P1,P2;
end;

Lm11:
  for A be non trivial set,B be set,
  Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
  yo2 be Function of Bo2,A st
  not Bo2 c= Bo1 holds
  ex f be Function of B,A st f|Bo1 = yo1 & f|Bo2 <> yo2
  proof
    let A be non trivial set, B be set,
    Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
    yo2 be Function of Bo2,A;
    assume not Bo2 c= Bo1;
    then consider x0 be set such that
D1: x0 in Bo2 & not x0 in Bo1 by TARSKI:def 3;
    ex y0 be set st y0 in A & y0 <> yo2.x0
    proof
      consider x,y be set such that
D21: x in A & y in A & x <> y by ZFMISC_1:def 10;
      per cases;
      suppose C1:yo2.x0 = x;
      take y;
      thus thesis by C1,D21;
    end;
    suppose C2:yo2.x0 <> x;
    take x;
    thus thesis by C2,D21;
  end;
end;
  then consider y0 be set such that
D2: y0 in A & y0 <> yo2.x0;
  defpred C[set] means $1 in Bo1;
  deffunc F(set) = yo1.$1;
  deffunc G(set) = y0;
D3: for x be set st x in B holds
  (C[ x] implies F(x) in A) & (not C[ x] implies G(x) in A)
  by D2,FUNCT_2:7;
  consider f be Function of B, A such that
D4: for x be set st x in B holds
  (C[ x] implies f.x = F(x)) & (not C[ x] implies f.x = G(x))
  from FUNCT_2:sch 5(D3);
P1: dom yo1 = Bo1 by FUNCT_2:def 1
           .= B /\ Bo1 by XBOOLE_1:28
           .= dom f /\ Bo1 by FUNCT_2:def 1;
  now let z be set;
  assume z in dom yo1;
  then z in Bo1;
  hence yo1.z = f.z by D4;
end; then
P2:f|Bo1 = yo1 by P1, FUNCT_1:68;
P3: x0 in dom yo2 by D1,FUNCT_2:def 1;
  f.x0 <> yo2.x0 by D2,D4,D1; then
  f|Bo2 <> yo2 by P3, FUNCT_1:68;
  hence thesis by P2;
end;

Lm12:
  for A be non trivial set, B be set,
  Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
  yo2 be Function of Bo2,A st
  Bo1 <> Bo2 & Bo2 c= Bo1 holds
  ex f be Function of B,A
  st f|Bo2 = yo2 & f|Bo1 <> yo1
  proof
    let A be non trivial set, B be set,
    Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
    yo2 be Function of Bo2,A;
    assume Bo1 <> Bo2 & Bo2 c= Bo1; then
    Bo2 c< Bo1 by XBOOLE_0:def 8; then
    consider x0 be set such that
D1: x0 in Bo1 & not x0 in Bo2 by XBOOLE_0:6;
    ex y0 be set st
    y0 in A & y0 <> yo1.x0
    proof
      consider x,y be set such that
D21: x in A & y in A & x <> y by ZFMISC_1:def 10;
      per cases;
      suppose C1:yo1.x0 = x;
      take y;
      thus thesis by C1,D21;
    end;
    suppose C2:yo1.x0 <> x;
    take x;
    thus thesis by C2,D21;
  end;
end;
  then consider y0 be set such that
D2: y0 in A & y0 <> yo1.x0;
  defpred C[set] means $1 in Bo2;
  deffunc F(set) = yo2.$1;
  deffunc G(set) = y0;
D3: for x be set st x in B holds
  (C[ x] implies F(x) in A) & (not C[ x] implies G(x) in A)
  by D2,FUNCT_2:7;
  consider f be Function of B, A such that
D4: for x be set st x in B holds
  (C[ x] implies f.x = F(x)) & (not C[ x] implies f.x = G(x))
  from FUNCT_2:sch 5(D3);
P1: dom yo2 = Bo2 by FUNCT_2:def 1
           .= B /\ Bo2 by XBOOLE_1:28
           .= dom f /\ Bo2 by FUNCT_2:def 1;
  now let z be set;
  assume z in dom yo2;
  then z in Bo2;
  hence yo2.z = f.z by D4;
end;
  then
P2: f|Bo2 = yo2 by P1, FUNCT_1:68;
P3: x0 in dom yo1 by D1,FUNCT_2:def 1;
  f.x0 <> yo1.x0 by D2,D4,D1;
  then
  f|Bo1 <> yo1 by P3, FUNCT_1:68;
  hence thesis by P2;
end;

Lm2:
  for A be non trivial set,B be set,
  Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
  yo2 be Function of Bo2,A st
  Bo1 <> Bo2 holds
  { y where y is Function of B,A : y|Bo1 = yo1 } <>
  { y where y is Function of B,A : y|Bo2 = yo2 }
  proof
    let A be non trivial set, B be set,
    Bo1,Bo2 be Subset of B,yo1 be Function of Bo1,A,
    yo2 be Function of Bo2,A;
    assume
A1: Bo1 <> Bo2;
    per cases;
    suppose not Bo2 c= Bo1; then
    consider f be Function of B,A such that
A2: f|Bo1 = yo1 & f|Bo2 <> yo2 by Lm11;
    not f in { y where y is Function of B,A : y|Bo2 = yo2 }
    proof
      assume f in { y where y is Function of B,A : y|Bo2 = yo2 };
      then ex y be Function of B,A st
      f=y & y|Bo2 = yo2;
      hence contradiction by A2;
    end;
    hence thesis by A2;
    end;
  suppose Bo2 c= Bo1;
  then
  consider f be Function of B,A such that
A2: f|Bo2 = yo2 & f|Bo1 <> yo1 by A1,Lm12;
  not f in { y where y is Function of B,A : y|Bo1 = yo1 }
  proof
    assume f in { y where y is Function of B,A : y|Bo1 = yo1 };
    then ex y be Function of B,A st
    f=y & y|Bo1 = yo1;
    hence contradiction by A2;
  end;
  hence thesis by A2;
  end;
end;

theorem LM3:
  for A be non trivial set, B be set,
  Bo1 be set, yo1 being Function of Bo1,A,
  Bo2 be set, yo2 being Function of Bo2,A
  st
   Bo1 c= B & Bo2 c= B
  & cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2)
  holds Bo1=Bo2 & yo1=yo2
  proof
    let A be non trivial set, B be set,
    Bo1 be set,yo1 being Function of Bo1,A,
    Bo2 be set,yo2 being Function of Bo2,A;
    assume
AS: Bo1 c= B & Bo2 c= B & cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2);
P1: { y where y is Function of B,A : y|Bo1 = yo1 }
    = cylinder0(A,B,Bo1,yo1) by DefX01,AS;
P2: { y where y is Function of B,A : y|Bo2 = yo2 }
    = cylinder0(A,B,Bo2,yo2) by DefX01,AS;
    hence
 Bo1=Bo2 by Lm2,AS,P1;
    consider y0 be set such that
P4: y0 in { y where y is Function of B,A : y|Bo1 = yo1 }
     by P1,XBOOLE_0:def 1;
    consider y be Function of B,A such that
P5: y0=y & y|Bo1 = yo1 by P4;
    consider w be Function of B,A such that
P6: y0=w & w|Bo2 = yo2 by P1,P2,AS,P4;
  thus yo1=yo2 by Lm2,AS,P1,P2,P5,P6;
end;

theorem LM4:
  for A1,A2 be non empty set, B1,B2 be set
  st A1 c= A2 & B1 c= B2
  ex F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) st
  for x be set st x in thin_cylinders(A1,B1)
  ex Bo being Subset of B1,
  yo1 being Function of Bo,A1,
  yo2 being Function of Bo,A2
  st Bo is finite & yo1=yo2 &
  x=cylinder0(A1,B1,Bo,yo1) &
  F.x=cylinder0(A2,B2,Bo,yo2)
  proof
    let A1,A2 be non empty set, B1,B2 be set;
    assume
AS: A1 c= A2 & B1 c= B2;
    defpred P[set,set] means
    ex Bo being Subset of B1,yo1 being Function of Bo,A1,
    yo2 being Function of Bo,A2
    st Bo is finite & yo1=yo2 &
    $1=cylinder0(A1,B1,Bo,yo1) &
    $2=cylinder0(A2,B2,Bo,yo2);
P1: now let x be set;
    assume x in thin_cylinders(A1,B1); then
    ex D be Subset of Funcs(B1,A1)
    st x=D & D is thin_cylinder of A1,B1; then
    reconsider D1=x as thin_cylinder of A1,B1;
    consider Bo being Subset of B1,yo1 being Function of Bo,A1 such that
P2: Bo is finite & D1=cylinder0(A1,B1,Bo,yo1) by Def21;
D13: Bo c= B2 by AS,XBOOLE_1:1;
    reconsider yo2=yo1 as Function of Bo,A2 by AS, FUNCT_2:9;
    set D2= cylinder0(A2,B2,Bo,yo2);
XXX: D2 is thin_cylinder of A2,B2 by P2,D13,Def21;
    reconsider D2 as set;
    take D2;
    thus D2 in thin_cylinders(A2,B2) & P[x,D2] by P2,XXX;
  end;
  consider F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2)
  such that
P2: for x be set st x in thin_cylinders(A1,B1)
  holds P[x,F.x] from FUNCT_2:sch 1(P1);
  take F;
  thus thesis by P2;
end;

theorem ThMX02:
  for A1,A2 be non empty set, B1,B2 be set
  ex G be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1) st
  for x be set st x in thin_cylinders(A2,B2)
  ex Bo2 being Subset of B2,Bo1 being Subset of B1,
  yo1 being Function of Bo1,A1,
  yo2 being Function of Bo2,A2
  st Bo1 is finite & Bo2 is finite
  & Bo1=B1 /\ Bo2 /\ (yo2"A1) & yo1=yo2 | Bo1 &
  x= cylinder0(A2,B2,Bo2,yo2) &
  G.x =cylinder0(A1,B1,Bo1,yo1)
  proof
    let A1,A2 be non empty set, B1,B2 be set;
    defpred P[set,set] means
    ex Bo2 being Subset of B2,Bo1 being Subset of B1,
    yo1 being Function of Bo1,A1,
    yo2 being Function of Bo2,A2 st Bo1 is finite & Bo2 is finite
    & Bo1=B1 /\ Bo2 /\ (yo2"A1)
    & yo1=yo2 | Bo1
    & $1=cylinder0(A2,B2,Bo2,yo2)
    & $2=cylinder0(A1,B1,Bo1,yo1);
P1: now let x be set;
    assume x in thin_cylinders(A2,B2); then
    ex D be Subset of Funcs(B2,A2) st x=D & D is thin_cylinder of A2,B2;
    then reconsider D2=x as thin_cylinder of A2,B2;
    consider Bo2 being Subset of B2,yo2 being Function of Bo2,A2 such that
P2: Bo2 is finite &
    D2=cylinder0(A2,B2,Bo2,yo2) by Def21;
    set Bo1=B1 /\ Bo2 /\ (yo2"A1);
XXX: Bo1 c= B1 /\ Bo2 by XBOOLE_1:17;
    B1 /\ Bo2 c= B1 by XBOOLE_1:17;then
D13: Bo1 c= B1 by XXX,XBOOLE_1:1;
    B1 /\ Bo2 c= Bo2 by XBOOLE_1:17; then
YYY: Bo1 c= Bo2 by XXX,XBOOLE_1:1;
    set yo1=yo2 | Bo1;
ZZZ: yo1 is Function of Bo1, A2 by YYY,FUNCT_2:38;
    W1:yo2.: (yo2"A1) c= A1 by FUNCT_1:145;
    W2: rng yo1 = yo2.: Bo1 by RELAT_1:148;
    yo2.: Bo1 c= yo2.: (yo2"A1) by RELAT_1:156,XBOOLE_1:17; then
    yo2.: Bo1 c= A1 by XBOOLE_1:1,W1; then
    reconsider yo1 as Function of Bo1,A1 by FUNCT_2:8,ZZZ,W2;
    set D1= cylinder0(A1,B1,Bo1,yo1);
XXX: D1 is thin_cylinder of A1,B1 by D13,P2,Def21;
    reconsider D1 as set;
    take D1;
    thus D1 in thin_cylinders(A1,B1) & P[x,D1] by P2,XXX,D13;
  end;
  consider G be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1)
  such that
P2: for x be set st x in thin_cylinders(A2,B2)
  holds P[x,G.x] from FUNCT_2:sch 1(P1);
  take G;
  thus thesis by P2;
end;

definition
  let A1,A2 be non trivial set, B1,B2 be set;
  assume AS: (ex x,y be set st x <> y & x in A1 & y in A1) &
  A1 c= A2 & B1 c= B2;
  func Extcylinders(A1,B1,A2,B2) ->
  Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) means
  for x be set st x in thin_cylinders(A1,B1)
  ex Bo being Subset of B1,
  yo1 being Function of Bo,A1,
  yo2 being Function of Bo,A2
  st Bo is finite & yo1=yo2 &
  x=cylinder0(A1,B1,Bo,yo1) &
  it.x=cylinder0(A2,B2,Bo,yo2);
  existence by LM4,AS;
  uniqueness
  proof
    let F1,F2 be Function of thin_cylinders(A1,B1),
    thin_cylinders(A2,B2);
    assume
AS1: for x be set st x in thin_cylinders(A1,B1)
    ex Bo being Subset of B1,
    yo1 being Function of Bo,A1,
    yo2 being Function of Bo,A2
    st Bo is finite & yo1=yo2 &
    x=cylinder0(A1,B1,Bo,yo1) &
    F1.x=cylinder0(A2,B2,Bo,yo2);
    assume
AS2: for x be set st x in thin_cylinders(A1,B1)
    ex Bo being Subset of B1,
    yo1 being Function of Bo,A1,
    yo2 being Function of Bo,A2
    st Bo is finite & yo1=yo2 &
    x=cylinder0(A1,B1,Bo,yo1) &
    F2.x=cylinder0(A2,B2,Bo,yo2);
    now let x be set;
    assume AS3: x in thin_cylinders(A1,B1);
    consider Bo1 being Subset of B1,
    yo11 being Function of Bo1,A1,
    yo21 being Function of Bo1,A2 such that
P1: Bo1 is finite & yo11=yo21 &
    x=cylinder0(A1,B1,Bo1,yo11) &
    F1.x=cylinder0(A2,B2,Bo1,yo21) by AS3,AS1;
    consider Bo2 being Subset of B1,
    yo12 being Function of Bo2,A1,
    yo22 being Function of Bo2,A2 such that
P2: Bo2 is finite & yo12=yo22 &
    x=cylinder0(A1,B1,Bo2,yo12) &
    F2.x=cylinder0(A2,B2,Bo2,yo22) by AS3,AS2;
P3: Bo1 = Bo2 & yo11 = yo12 by LM3,P1,P2;
    thus F1.x=F2.x by P1,P2,P3;
  end;
  hence F1=F2 by FUNCT_2:18;
  end;
end;

definition
  let A1 be non empty set, A2 be non trivial set, B1,B2 be set;
  assume
A1 c= A2 & B1 c= B2;
  func Ristcylinders(A1,B1,A2,B2) ->
  Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1) means
  for x be set st x in thin_cylinders(A2,B2)
  ex Bo2 being Subset of B2,Bo1 being Subset of B1,
  yo1 being Function of Bo1,A1,
  yo2 being Function of Bo2,A2
  st Bo1 is finite & Bo2 is finite
  & Bo1=B1 /\ Bo2 /\ (yo2"A1)
  & yo1=yo2 | Bo1 &
  x = cylinder0(A2,B2,Bo2,yo2) &
  it.x =cylinder0(A1,B1,Bo1,yo1);
  existence by ThMX02;
  uniqueness
  proof
    let F1,F2 be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1);
    assume
AS1: for x be set st x in thin_cylinders(A2,B2)
    ex Bo21 being Subset of B2,Bo11 being Subset of B1,
    yo11 being Function of Bo11,A1,
    yo21 being Function of Bo21,A2
    st Bo11 is finite & Bo21 is finite
    & Bo11=B1 /\ Bo21 /\ (yo21"A1)
    & yo11=yo21 | Bo11 &
    x= cylinder0(A2,B2,Bo21,yo21) &
    F1.x =cylinder0(A1,B1,Bo11,yo11);
    assume
AS2: for x be set st x in thin_cylinders(A2,B2)
    ex Bo22 being Subset of B2,Bo12 being Subset of B1,
    yo12 being Function of Bo12,A1,
    yo22 being Function of Bo22,A2
    st Bo12 is finite & Bo22 is finite
    & Bo12=B1 /\ Bo22 /\ (yo22"A1) & yo12=yo22 | Bo12 &
    x= cylinder0(A2,B2,Bo22,yo22) &
    F2.x =cylinder0(A1,B1,Bo12,yo12);
    now let x be set;
    assume
AS3: x in thin_cylinders(A2,B2);
    consider Bo21 being Subset of B2,Bo11 being Subset of B1,
    yo11 being Function of Bo11,A1,
    yo21 being Function of Bo21,A2 such that
P1: Bo11 is finite & Bo21 is finite
    & Bo11=B1 /\ Bo21 /\ (yo21"A1) & yo11=yo21 | Bo11 &
    x= cylinder0(A2,B2,Bo21,yo21) &
    F1.x =cylinder0(A1,B1,Bo11,yo11) by AS3,AS1;
    consider Bo22 being Subset of B2,Bo12 being Subset of B1,
    yo12 being Function of Bo12,A1,
    yo22 being Function of Bo22,A2 such that
P2: Bo12 is finite & Bo22 is finite
    & Bo12=B1 /\ Bo22 /\ (yo22"A1) & yo12=yo22 | Bo12 &
    x= cylinder0(A2,B2,Bo22,yo22) &
    F2.x =cylinder0(A1,B1,Bo12,yo12) by AS3,AS2;
    P3: Bo21 = Bo22 & yo21 = yo22 by LM3,P1,P2;
    thus F1.x=F2.x by P1,P2,P3;
  end;
  hence F1=F2 by FUNCT_2:18;
  end;
end;

definition
  let A be non trivial set,B be set;
  let D be thin_cylinder of A,B;
  func loc(D) -> finite Subset of B means
  ex Bo being Subset of B,yo being Function of Bo,A st
  Bo is finite &
  D = { y where y is Function of B,A : y|Bo = yo }
  & it = Bo;
  existence
  proof
    consider Bo be Subset of B, yo be Function of Bo,A such that
A1: Bo is finite &
    D = { y where y is Function of B,A : y|Bo = yo } by LM1;
    thus thesis by A1;
  end;
  uniqueness by Lm2;
end;

begin :: Colored Petri nets

definition
  let A1,A2 be non trivial set, B1,B2 be set;
  let C1,C2 be non trivial set, D1,D2 be set;
  let F be Function of thin_cylinders(A1,B1), thin_cylinders(C1,D1);
  func CylinderFunc(A1,B1,A2,B2,C1,D1,C2,D2,F) -> Function
     of thin_cylinders(A2,B2), thin_cylinders(C2,D2) equals
  Extcylinders(C1,D1,C2,D2)*F*Ristcylinders(A1,B1,A2,B2);
  correctness;
end;

definition
  struct (PT_net_Str) Colored_PT_net_Str
  (# Places, Transitions -> non empty set,
  S-T_Arcs -> non empty Relation of the Places,the Transitions,
  T-S_Arcs -> non empty Relation of the Transitions, the Places,
  ColoredSet  -> non empty finite set,
  firing-rule -> Function #);
end;

definition
  let CPNT be Colored_PT_net_Str;
  let t0 be transition of CPNT;
  attr t0 is outbound means :Def7:
  {t0}*' = {};
end;

definition
  let CPNT1 be Colored_PT_net_Str;
  func Outbds(CPNT1) -> Subset of the Transitions of CPNT1 equals
  {x where x is transition of CPNT1 : x is outbound };
  coherence
  proof
    {x where x is transition of CPNT1 : x is outbound }
    c= the Transitions of CPNT1
    proof
      let z be set;
      assume z in {x where x is transition of CPNT1 : x is outbound };
      then ex x be transition of CPNT1 st z=x & x is outbound;
      hence z in the Transitions of CPNT1;
    end;
    hence thesis;
  end;
end;

definition
  let CPNT be Colored_PT_net_Str;
  attr CPNT is Colored-PT-net-like means :Def4:
  dom (the firing-rule of CPNT)
  c= (the Transitions of CPNT) \ Outbds(CPNT) &
  for t being transition of CPNT
  st t in dom (the firing-rule of CPNT) holds
  ex CS be non empty Subset of the ColoredSet of CPNT,
  I be Subset of *'{t},
  O be Subset of {t}*' st (the firing-rule of CPNT ).t
  is Function of thin_cylinders(CS,I), thin_cylinders(CS,O);
end;

theorem
  for CPNT be Colored_PT_net_Str,
  t being transition of CPNT st
  CPNT is Colored-PT-net-like &
  t in dom (the firing-rule of CPNT) holds
  ex CS be non empty Subset of the ColoredSet of CPNT,
  I be Subset of *'{t},
  O be Subset of {t}*' st
  (the firing-rule of CPNT ).t
  is Function of thin_cylinders(CS,I),
  thin_cylinders(CS,O) by Def4;

theorem LM6:
  for CPNT1,CPNT2 be Colored_PT_net_Str,
  t1 be transition of CPNT1,t2 be transition of CPNT2 st
  the Places of CPNT1 c= the Places of CPNT2
  & the Transitions of CPNT1 c= the Transitions of CPNT2
  & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2
  & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2
  & t1=t2 holds
  *'{t1} c= *'{t2} & {t1}*' c= {t2}*'
  proof
    let CPNT1,CPNT2 be Colored_PT_net_Str,
    t1 be transition of CPNT1,t2 be transition of CPNT2;
    assume
AS1: the Places of CPNT1 c= the Places of CPNT2
    & the Transitions of CPNT1 c= the Transitions of CPNT2
    & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2
    & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1=t2;
    thus *'{t1} c= *'{t2}
    proof
      let x be set;
      assume x in *'{t1}; then
      consider s be place of CPNT1 such that
A1:   x=s &
      ex f being S-T_arc of CPNT1,
      w being transition of CPNT1 st w in {t1} & f = [s,w];
      consider f being S-T_arc of CPNT1,
      w being transition of CPNT1 such that
A2:   w in {t2} & f = [x,w] by AS1,A1;
P1:   f is S-T_arc of CPNT2 by AS1,TARSKI:def 3;
      x is place of CPNT2 by A1,AS1,TARSKI:def 3;
      hence x in *'{t2} by P1,A2;
  end;
    let x be set;
    assume x in {t1}*';
    then consider s be place of CPNT1 such that
A1: x=s & ex f being T-S_arc of CPNT1,
    w being transition of CPNT1 st w in {t1} & f = [w,s];
    consider f being T-S_arc of CPNT1,
    w being transition of CPNT1 such that
A2: w in {t2} & f = [w,x] by A1,AS1;
P1: f is T-S_arc of CPNT2 by AS1,TARSKI:def 3;
    x is place of CPNT2 by A1,AS1,TARSKI:def 3;
    hence x in {t2}*' by P1,A2;
end;

LM7:
  for f1,f2,f3,f4,g be Function
  st dom f1 /\ dom f2 = {} &
  dom f1 /\ dom f2 = {} &
  dom f1 /\ dom f3 = {} &
  dom f1 /\ dom f4 = {} &
  dom f2 /\ dom f3 = {} &
  dom f2 /\ dom f4 = {} &
  dom f3 /\ dom f4 = {} &
  g=f1+*f2+*f3+*f4
  holds
  (for x be set st x in dom f1 holds g.x=f1.x) &
  (for x be set st x in dom f2 holds g.x=f2.x) &
  (for x be set st x in dom f3 holds g.x=f3.x) &
  (for x be set st x in dom f4 holds g.x=f4.x)
  proof
    let f1,f2,f3,f4,g be Function;
    assume
AS: dom f1 /\ dom f2 = {} &
    dom f1 /\ dom f2 = {} &
    dom f1 /\ dom f3 = {} &
    dom f1 /\ dom f4 = {} &
    dom f2 /\ dom f3 = {} &
    dom f2 /\ dom f4 = {} &
    dom f3 /\ dom f4 = {} &
    g=f1+*f2+*f3+*f4;
    set f12 = f1+*f2;
    set f123=f1+*f2+*f3;
    thus for x be set st x in dom f1 holds g.x=f1.x
    proof
      let x be set;
      assume AS1: x in dom f1;
      then
P1: not x in dom f4 by AS,XBOOLE_0:def 4;
P2: not x in dom f3 by AS1,AS,XBOOLE_0:def 4;
P3: not x in dom f2 by AS1,AS,XBOOLE_0:def 4;
      thus g.x = f123.x by AS,FUNCT_4:12,P1
         .= f12.x by FUNCT_4:12,P2
         .= f1.x by FUNCT_4:12,P3;
    end;
    thus for x be set st x in dom f2 holds g.x=f2.x
    proof
      let x be set;
      assume
AS1: x in dom f2; then
P1: not x in dom f4 by AS,XBOOLE_0:def 4;
P2: not x in dom f3 by AS1,AS,XBOOLE_0:def 4;
      thus g.x = f123.x by AS,FUNCT_4:12,P1
         .= f12.x by FUNCT_4:12,P2
         .= f2.x by FUNCT_4:14,AS1;
    end;
    thus for x be set st x in dom f3 holds g.x=f3.x
      proof
        let x be set;
        assume AS1: x in dom f3; then
        not x in dom f4 by AS,XBOOLE_0:def 4;
        hence g.x = f123.x by AS,FUNCT_4:12
           .= f3.x by FUNCT_4:14,AS1;
      end;
      thus for x be set st x in dom f4 holds g.x=f4.x by AS,FUNCT_4:14;
    end;

LM8:
  for A,B,C,D,X1,X2,X3,X4 be set
  st A /\ B = {} & C c= A & D c= B
  & X1 c= A \ C & X2 c= B \ D & X3=C & X4= D holds
  X1 /\ X2 = {} &
  X1 /\ X3 = {} &
  X1 /\ X4 = {} &
  X2 /\ X3 = {} &
  X2 /\ X4 = {} &
  X3 /\ X4 = {}
  proof
    let A,B,C,D,X1,X2,X3,X4 be set;
    assume
AS: A /\ B = {} & C c= A & D c= B
    & X1 c= A \ C & X2 c= B \ D & X3=C & X4= D;
P1: (A \ C) /\ (B \ D) c= A /\ B by XBOOLE_1:27;
    X1 /\ X2 c= (A \ C) /\ (B \ D) by AS,XBOOLE_1:27;
    hence X1 /\ X2 = {} by AS,P1;
P2: (A \ C) /\ C = (C /\ A) \ C by XBOOLE_1:49;
    C /\ A c= C by XBOOLE_1:17;
    then (A \ C) /\ C= {} by XBOOLE_1:37,P2;
    hence X1 /\ X3 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
    (A \ C) /\ D = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
    hence X1 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
    (B \ D) /\ C = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
    hence X2 /\ X3 = {} by AS,XBOOLE_1:27,XBOOLE_1:3;
P6: (B \ D) /\ D = (B /\ D) \ D by XBOOLE_1:49;
    B /\ D c= D by XBOOLE_1:17;
    then (B \ D) /\ D= {} by P6,XBOOLE_1:37;
    hence X2 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
    thus X3 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
  end;

registration
  cluster strict Colored-PT-net-like Colored_PT_net_Str;
  existence
  proof
    consider a,b,red,yellow,blue be set;
    set PLA={0};
    set TRA={a};
    set CS = {red,yellow,blue};
    set STA = [:PLA,TRA:];
    reconsider STA as non empty Relation of PLA,TRA by RELSET_1:def 1;
    set TSA= [:TRA,PLA:];
    reconsider TSA as non empty Relation of TRA,PLA by RELSET_1:def 1;
    consider fa be Function of thin_cylinders(CS,{0}),
                                 thin_cylinders(CS,{0});
    set f= ({a} --> fa);
    take CPNT = Colored_PT_net_Str
    (# PLA,TRA,STA,TSA, CS,f #);
A0: dom f = {a} by FUNCOP_1:19;
    now let x be set;
    assume
A11: x in dom (the firing-rule of CPNT);
A13: x=a by A0,A11,TARSKI:def 1;
    reconsider a1=a as transition of CPNT by TARSKI:def 1;
    0 in PLA & a in TRA by TARSKI:def 1;
    then [a1,0] in TSA by ZFMISC_1:106;
    then
aa: not {a1}*' = {} by PETRI:8;
    not a1 in Outbds(CPNT)
    proof
      assume a1 in Outbds(CPNT); then
      ex x be transition of CPNT st a1=x & x is outbound;
      hence contradiction by aa,Def7;
    end;
    hence x in (the Transitions of CPNT) \ Outbds(CPNT) by A13,XBOOLE_0:def 5;
  end;
  then
A1: dom (the firing-rule of CPNT) c=
  (the Transitions of CPNT) \ Outbds(CPNT) by TARSKI:def 3;
  now let t be transition of CPNT;
  assume t in dom (the firing-rule of CPNT);
P1: t= a by TARSKI:def 1;
P2: 0 in PLA & a in TRA by TARSKI:def 1;
  then [a,0] in TSA by ZFMISC_1:106; then
pp: 0 in {t} *' by PETRI:8,P1;
  [0,a] in STA by ZFMISC_1:106,P2; then
pa: 0 in *'{t} by PETRI:6,P1;
  CS c= CS;
  then reconsider CS1= CS as non empty Subset of the ColoredSet of CPNT;
  reconsider I = {0} as Subset of *'{t} by pa,ZFMISC_1:37;
  reconsider O = {0} as Subset of {t} *' by pp,ZFMISC_1:37;
P7: f.t =fa by FUNCOP_1:13;
  fa is Function of thin_cylinders(CS1,I), thin_cylinders(CS1,O );
  hence ex CS1 be non empty Subset of the ColoredSet of CPNT,
  I be Subset of *'{t}, O be Subset of {t}*' st (the firing-rule of CPNT ).t
  is Function of thin_cylinders(CS1,I), thin_cylinders(CS1,O ) by P7;
  end;
  hence thesis by A1,Def4;
  end;
end;

definition
  mode Colored-PT-net is Colored-PT-net-like Colored_PT_net_Str;
end;

reserve CPNT for Colored-PT-net;

begin :: Outbound transitions of CPNT

definition
  let CPNT1, CPNT2 be Colored_PT_net_Str;
  pred CPNT1 misses CPNT2 means :Def7A:
  (the Places of CPNT1) /\ (the Places of CPNT2 ) = {} &
  (the Transitions of CPNT1) /\ (the Transitions of CPNT2) = {};
  symmetry;
end;

begin :: Connecting mapping for CPNT1,CPNT2

definition
  let CPNT1 be Colored_PT_net_Str;
  let CPNT2 be Colored_PT_net_Str;
  mode connecting-mapping of CPNT1,CPNT2 means :Def8:
  ex O12 be Function of Outbds(CPNT1), the Places of CPNT2,
  O21 be Function of Outbds(CPNT2), the Places of CPNT1
  st it=[O12,O21];
  correctness
  proof
    consider O12 be Function of Outbds(CPNT1), the Places of CPNT2,
             O21 be Function of Outbds(CPNT2), the Places of CPNT1;
    set Z = [O12,O21];
    take Z;
    thus thesis;
  end;
end;

begin :: Connecting firing rule for CPNT1,CPNT2

definition
  let CPNT1, CPNT2 be Colored-PT-net;
  let O be connecting-mapping of CPNT1,CPNT2;
  mode connecting-firing-rule of CPNT1,CPNT2,O means :Def9:
  ex q12,q21 be Function,
  O12 be Function of Outbds(CPNT1), the Places of CPNT2,
  O21 be Function of Outbds(CPNT2), the Places of CPNT1
  st O=[O12,O21]
  & dom q12=Outbds(CPNT1) & dom q21=Outbds(CPNT2) &
  ( for t01 be 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 be 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) ) ) & it=[q12,q21];
  correctness
  proof
    consider O12 be Function of Outbds(CPNT1), the Places of CPNT2,
    O21 be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: O = [O12,O21] by Def8;
    set TO1 = Outbds(CPNT1);
    set TO2 = Outbds(CPNT2);
    set K1=bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT1);
    set K2=bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT1);
    set L1=bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT2);
    set L2=bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT2);
    set Y1= PFuncs(K1,K2);
    set Y2= PFuncs(L1,L2);
    defpred P[set,set] means
    ex t01 be 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) );
P2: for x be set st x in TO1 ex y be set st y in Y1 & P[x,y]
    proof
      let x be set;
      assume x in TO1; then
      consider t01 be transition of CPNT1 such that
P21: x=t01 & t01 is outbound;
      set  t1=*'{t01};
      set  t2=Im(O12,t01);
      consider y be Function of
      thin_cylinders ( the ColoredSet of CPNT1, t1),
      thin_cylinders ( the ColoredSet of CPNT1, t2);
      take y;
      set H1= thin_cylinders ( the ColoredSet of CPNT1, t1);
      set H2= thin_cylinders ( the ColoredSet of CPNT1, t2);
XH1: H1 c=
      bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT1) by LmThin;
XH2: H2 c=
      bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT1) by LmThin;
J1: y in Funcs(H1,H2) by FUNCT_2:11;
      Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:141; then
J2:y in PFuncs(H1,H2) by J1;
      PFuncs(H1,H2) c= PFuncs(K1,K2) by PARTFUN1:128,XH1,XH2;
      hence thesis by P21,J2;
    end;
    consider q12 be Function of TO1,Y1 such that
P3: for x be set st x in TO1 holds P[x,q12.x] from FUNCT_2:sch 1(P2);
P4: now let tt01 be transition of CPNT1;
    assume tt01 is outbound;
    then tt01 in TO1; then
    ex t01 be 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 P3;
    hence q12.tt01 is Function of
    thin_cylinders ( the ColoredSet of CPNT1, *'{tt01}),
    thin_cylinders ( the ColoredSet of CPNT1, Im(O12,tt01) );
  end;
  defpred R[set,set] means ex t02 be 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));
R2: for x be set st x in TO2 ex y be set st y in Y2 & R[x,y]
  proof
    let x be set;
    assume x in TO2; then
    consider t02 be transition of CPNT2 such that
R21: x=t02 & t02 is outbound;
    set t1=*'{t02};
    set t2= Im(O21,t02);
    consider y be Function of
    thin_cylinders ( the ColoredSet of CPNT2, t1),
    thin_cylinders ( the ColoredSet of CPNT2, t2);
    take y;
    set H1= thin_cylinders ( the ColoredSet of CPNT2, t1);
    set H2= thin_cylinders ( the ColoredSet of CPNT2, t2);
XH1: H1 c=
    bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT2) by LmThin;
XH2: H2 c=
    bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT2) by LmThin;
J1: y in Funcs(H1,H2) by FUNCT_2:11;
    Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:141;
    then
J2:y in PFuncs(H1,H2) by J1;
    PFuncs(H1,H2) c= PFuncs(L1,L2) by PARTFUN1:128,XH1,XH2;
    hence thesis by R21,J2;
    end;
    consider q21 be
    Function of TO2,Y2 such that
R3: for x be set st x in TO2 holds R[x,q21.x] from FUNCT_2:sch 1(R2);
R4:now let tt02 be transition of CPNT2;
    assume tt02 is outbound;
    then tt02 in TO2; then
    ex t02 be 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 R3;
    hence q21.tt02 is Function of
    thin_cylinders ( the ColoredSet of CPNT2, *'{tt02}),
    thin_cylinders ( the ColoredSet of CPNT2, Im(O21,tt02));
    end;
    take [q12,q21];
    dom q12=Outbds(CPNT1) & dom q21=Outbds(CPNT2) by FUNCT_2:def 1;
    hence thesis by P1,P4,R4;
  end;
end;

begin :: Synthesis of CPNT1,CPNT2

definition
  let CPNT1, CPNT2 be Colored-PT-net;
  let O be connecting-mapping of CPNT1,CPNT2;
  let q be connecting-firing-rule of CPNT1,CPNT2,O;
  assume
AS: CPNT1 misses CPNT2;
  func synthesis(CPNT1, CPNT2,O,q) -> strict Colored-PT-net means
  ex q12,q21 be Function,
  O12 be Function of Outbds(CPNT1), the Places of CPNT2,
  O21 be Function of Outbds(CPNT2), the Places of CPNT1 st O=[O12,O21] &
  dom q12=Outbds(CPNT1) & dom q21=Outbds(CPNT2) &
  ( for t01 be 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 be 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) ) )
  & q=[q12,q21]
  & the Places of it = (the Places of CPNT1) \/ (the Places of CPNT2) &
  the Transitions of it =
  (the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
  the S-T_Arcs of it =
  (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
  the T-S_Arcs of it =
  (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/ O21 &
  the ColoredSet of it = (the ColoredSet of CPNT1)
  \/ (the ColoredSet of CPNT2) &
  the firing-rule of it =
  (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
  existence
  proof
    consider q12,q21 be Function,
    O12 be Function of Outbds(CPNT1), the Places of CPNT2,
    O21 be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: O=[O12,O21]
    & dom q12=Outbds(CPNT1) & dom q21=Outbds(CPNT2) &
    ( for t01 be 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 be 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) )) & q=[q12,q21]
             by Def9;
    reconsider P12 = (the Places of CPNT1) \/ (the Places of CPNT2)
    as non empty set;
    reconsider T12 = (the Transitions of CPNT1) \/ (the Transitions of CPNT2)
    as non empty set;
    (the Places of CPNT1) c= P12 & (the Transitions of CPNT1) c= T12
    by XBOOLE_1:7; then
    reconsider E1=(the S-T_Arcs of CPNT1) as Relation of P12,T12
    by RELSET_1:17;
    (the Places of CPNT2) c= P12 & (the Transitions of CPNT2) c= T12
    by XBOOLE_1:7; then
    reconsider E2=(the S-T_Arcs of CPNT2) as Relation of P12,T12
    by RELSET_1:17;
    E1 \/ E2 is Relation of P12,T12; then
    reconsider ST12= (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2)
    as non empty Relation of P12,T12;
    (the Transitions of CPNT1) c= T12 & (the Places of CPNT1) c= P12
    by XBOOLE_1:7; then
    reconsider E21=(the T-S_Arcs of CPNT1) as Relation of T12,P12
    by RELSET_1:17;
    (the Transitions of CPNT2) c= T12 & (the Places of CPNT2) c= P12
    by XBOOLE_1:7; then
    reconsider E22=(the T-S_Arcs of CPNT2) as Relation of T12,P12
    by RELSET_1:17;
    E21 \/ E22 is Relation of T12,P12; then
    reconsider TTS12= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
    as non empty Relation of T12,P12;
    (the Transitions of CPNT1) c= T12 by XBOOLE_1:7; then
L30: Outbds(CPNT1) c= T12 by XBOOLE_1:1;
    (the Transitions of CPNT2) c= T12 by XBOOLE_1:7; then
L31: Outbds(CPNT2) c= T12 by XBOOLE_1:1;
L32: the Places of CPNT2 c= P12 by XBOOLE_1:7;
L33: the Places of CPNT1 c= P12 by XBOOLE_1:7;
    reconsider E31=O12 as Relation of T12,P12 by L30,L32,RELSET_1:17;
    reconsider E32=O21 as  Relation of T12,P12 by L31,L33,RELSET_1:17;
    reconsider TS12= TTS12 \/ (E31 \/ E32) as non empty Relation of T12,P12;
    reconsider CS12 = (the ColoredSet of CPNT1)
    \/ (the ColoredSet of CPNT2) as non empty finite set;
    set CR12=
    (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
    set CPNT12=Colored_PT_net_Str (# P12,T12, ST12,TS12,CS12,CR12 #);
    set R1=the firing-rule of CPNT1;
    set R2=the firing-rule of CPNT2;
    set R3=q12;
    set R4=q21;
    P2: TS12= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)  \/ O12 \/O21
    by XBOOLE_1:4;
P22: now let x be set;
    assume x in dom CR12; then
    x in dom ( R1 +* R2 +* R3) or x in dom R4 by FUNCT_4:13; then
    x in dom ( R1 +*  R2 )
    or x in dom R3 or x in dom R4 by FUNCT_4:13;
    hence x in dom R1 or x in dom R2
    or x in dom R3 or x in dom R4 by FUNCT_4:13;
  end;
LM6T1: the Places of CPNT1 c= the Places of CPNT12 by XBOOLE_1:7;
LM6T2: (the Transitions of CPNT1) c= (the Transitions of CPNT12)
    by XBOOLE_1:7;
LM6T3: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
Q2: (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) c=
      the T-S_Arcs of CPNT12 by XBOOLE_1:7;
    (the T-S_Arcs of CPNT1)
    c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) by XBOOLE_1:7;
    then
LM6T4: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12
    by Q2,XBOOLE_1:1;
LM6S1: the Places of CPNT2 c= the Places of CPNT12 by XBOOLE_1:7;
LM6S2: (the Transitions of CPNT2) c= (the Transitions of CPNT12)
    by XBOOLE_1:7;
LM6S3: the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
Q2:(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
    c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
    (the T-S_Arcs of CPNT2)
    c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
    by XBOOLE_1:7;
    then
LM6S4: the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
    by Q2,XBOOLE_1:1;
LM7T1: (the Transitions of CPNT1) /\ (the Transitions of CPNT2)
    = {} by AS,Def7A;
LM7T4: dom (the firing-rule of CPNT1)
    c= (the Transitions of CPNT1) \ (dom q12) by P1,Def4;
LM7T5: dom (the firing-rule of CPNT2)
    c= (the Transitions of CPNT2) \ (dom q21) by P1,Def4;
LM7T:
    dom (the firing-rule of CPNT1) /\ dom (the firing-rule of CPNT2) = {} &
    dom (the firing-rule of CPNT1) /\ dom (the firing-rule of CPNT2) = {} &
    dom (the firing-rule of CPNT1) /\ dom q12 = {} &
    dom (the firing-rule of CPNT1) /\ dom q21 = {} &
    dom (the firing-rule of CPNT2) /\ dom q12 = {} &
    dom (the firing-rule of CPNT2) /\ dom q21 = {} &
    dom q12 /\ dom q21 ={} by LM8,LM7T1,P1,LM7T4,LM7T5;
s10:now let x be set;
    assume x in dom CR12; then
PP1: x in dom R1 or x in dom R2
    or x in dom R3 or x in dom R4 by P22;
    dom ( the firing-rule of CPNT1)
    c= (the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
PP2: dom ( the firing-rule of CPNT1) c= the Transitions of CPNT1
    by XBOOLE_1:1;
    dom ( the firing-rule of CPNT2)
    c= (the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
pp: dom ( the firing-rule of CPNT2) c= the Transitions of CPNT2
    by XBOOLE_1:1;
    thus x in (the Transitions of CPNT1) \/ (the Transitions of CPNT2)
    by XBOOLE_0:def 3,pp,P1,PP1,PP2;
  end; then
S10: dom (the firing-rule of CPNT12)
    c= the Transitions of CPNT12 by TARSKI:def 3;
SS1:for t being transition of CPNT12
    st t in dom (the firing-rule of CPNT12) holds
    ex CS be non empty Subset of the ColoredSet of CPNT12,
    I be Subset of *'{t}, O be Subset of {t}*' st
    (the firing-rule of CPNT12 ).t
    is Function of thin_cylinders(CS,I), thin_cylinders(CS,O)
    proof
      let t be transition of CPNT12;
      assume
SS2: t in dom (the firing-rule of CPNT12);
      now per cases by SS2,P22;
      suppose
S4: t in dom the firing-rule of CPNT1;
      dom ( the firing-rule of CPNT1) c=
      (the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
      reconsider t1 =t as  transition of CPNT1 by S4,TARSKI:def 3;
      consider CS1 be non empty Subset of the ColoredSet of CPNT1,
      I1 be Subset of *'{t1}, O1 be Subset of {t1}*' such that
T6: (the firing-rule of CPNT1).t1
      is Function of thin_cylinders(CS1,I1),
      thin_cylinders(CS1,O1) by Def4,S4;
      the ColoredSet of CPNT1 c= the ColoredSet of CPNT12 by XBOOLE_1:7;
      then reconsider
      CS = CS1 as non empty Subset of the ColoredSet of CPNT12
      by XBOOLE_1:1;
      *'{t1} c= *'{t} by LM6,LM6T1,LM6T2,LM6T3,LM6T4;
      then reconsider I =I1 as Subset of *'{t} by XBOOLE_1:1;
      {t1}*' c= {t}*' by LM6,LM6T1,LM6T2,LM6T3,LM6T4;
      then reconsider O =O1 as Subset of {t}*' by XBOOLE_1:1;
      (the firing-rule of CPNT12).t
      is Function of thin_cylinders(CS,I),
      thin_cylinders(CS,O) by S4,LM7,LM7T,T6;
      hence thesis;
    end;
    suppose
S5: t in dom ( the firing-rule of CPNT2);
    dom ( the firing-rule of CPNT2) c=
    (the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
    reconsider t1 = t as transition of CPNT2 by S5,TARSKI:def 3;
    consider CS1 be non empty Subset of the ColoredSet of CPNT2,
    I1 be Subset of *'{t1}, O1 be Subset of {t1}*' such that
T6: (the firing-rule of CPNT2).t1
    is Function of thin_cylinders(CS1,I1),
    thin_cylinders(CS1,O1) by Def4,S5;
    the ColoredSet of CPNT2 c= the ColoredSet of CPNT12 by XBOOLE_1:7; then
    reconsider CS = CS1 as non empty Subset of the ColoredSet of CPNT12
    by XBOOLE_1:1;
    *'{t1} c= *'{t} by LM6,LM6S1,LM6S2,LM6S3,LM6S4; then
    reconsider I =I1 as  Subset of *'{t} by XBOOLE_1:1;
    {t1}*' c= {t}*' by LM6,LM6S1,LM6S2,LM6S3,LM6S4; then
    reconsider O =O1 as Subset of {t}*' by XBOOLE_1:1;
    (the firing-rule of CPNT12).t
    is Function of thin_cylinders(CS,I),
    thin_cylinders(CS,O) by S5,LM7,LM7T,T6;
    hence thesis;
  end;
    suppose S6:  t in dom (q12);
    reconsider t1 =t as transition of CPNT1 by S6,P1;
    S610:ex x1 be transition of CPNT1 st t1=x1 & x1 is outbound by S6,P1;
T6: q12.t1 is Function of
    thin_cylinders ( the ColoredSet of CPNT1, *'{t1}),
    thin_cylinders ( the ColoredSet of CPNT1, Im(O12,t1) ) by P1,S610;
    reconsider CS = the ColoredSet of CPNT1
    as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
    reconsider I =*'{t1} as Subset of *'{t} by LM6,LM6T1,LM6T2,LM6T3,LM6T4;
    Im(O12,t1) c= {t}*'
    proof
      let x be set;
      assume
Z:     x in Im(O12,t1);
      then reconsider s = x as place of CPNT2;
A1:   [t1,s] in O12 by Z,RELSET_2:9;
A5: O12 c= E31 \/ E32 by XBOOLE_1:7;
      E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7; then
      O12 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5; then
      reconsider f= [t,s] as T-S_arc of CPNT12 by A1;
A4: s in the Places of CPNT2;
A31:the Places of CPNT2
      c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
      t in {t} & f=[t,s] by TARSKI:def 1;
      hence x in {t}*' by A31,A4;
  end;
      then reconsider O = Im(O12,t1) as Subset of {t}*';
      (the firing-rule of CPNT12).t
      is Function of thin_cylinders(CS,I),
      thin_cylinders(CS,O) by S6,LM7,LM7T,T6;
      hence thesis;
    end;
      suppose S7: t in dom (q21); then
      reconsider t1 = t as transition of CPNT2 by P1;
S610: ex x1 be transition of CPNT2 st t1=x1 & x1 is outbound by S7,P1;
T6: q21.t1 is Function of
      thin_cylinders (the ColoredSet of CPNT2, *'{t1}),
      thin_cylinders (the ColoredSet of CPNT2, Im(O21,t1) ) by P1,S610;
      reconsider CS = the ColoredSet of CPNT2
      as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
      reconsider
      I =*'{t1} as Subset of *'{t} by LM6,LM6S1,LM6S2,LM6S3,LM6S4;
      Im(O21,t1) c= {t}*'
      proof
        let x be set;
        assume
Z:        x in Im(O21,t1);
         then reconsider s=x as place of CPNT1;
A1:   [t1,s] in O21 by Z,RELSET_2:9;
A5: O21 c= E31 \/ E32 by XBOOLE_1:7;
        E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
        then
        reconsider f= [t,s] as T-S_arc of CPNT12 by TARSKI:def 3,A1,A5;
A4: s in the Places of CPNT1;
A31: the Places of CPNT1
        c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
        t in {t} & f=[t,s] by TARSKI:def 1;
        hence x in {t}*' by A31,A4;
      end;
      then reconsider O = Im(O21,t1) as Subset of {t}*';
      (the firing-rule of CPNT12).t
      is Function of thin_cylinders(CS,I),
      thin_cylinders(CS,O) by S7,LM7,LM7T,T6;
      hence thesis;
    end;
  end;
  hence thesis;
end;
    dom (the firing-rule of CPNT12)
    c= (the Transitions of CPNT12) \ Outbds(CPNT12)
    proof
      let x be set;
      assume
ASD:  x in dom (the firing-rule of CPNT12); then
      reconsider t=x as transition of CPNT12 by s10;
      set RR1=the firing-rule of CPNT1;
      set RR2=the firing-rule of CPNT2;
      set RR3=q12;
      set RR4=q21;
      now per cases by ASD,P22;
      suppose CAS1:t in dom RR1;
Q0: dom ( the firing-rule of CPNT1) c=
      (the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
Q1: t in the Transitions of CPNT1 & not t in Outbds(CPNT1)
      by CAS1,XBOOLE_0:def 5;
      reconsider t1 =t as transition of CPNT1 by Q0,CAS1,XBOOLE_0:def 5;
      not t1 is outbound by Q1;
      then {t1}*' <> {} by Def7;
      then
Q2:   ex g be set st g in {t1}*' by XBOOLE_0:def 1;
      {t1}*' c= {t}*' by LM6,LM6T1,LM6T2,LM6T3,LM6T4; then
      not ex w be transition of CPNT12 st t=w & w is outbound by Def7,Q2;
      hence not x in Outbds(CPNT12);
    end;
      suppose CAS2:t in dom RR2;
Q0:dom ( the firing-rule of CPNT2) c=
      (the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
Q1: t in the Transitions of CPNT2 & not t in Outbds(CPNT2)
      by CAS2,XBOOLE_0:def 5;
      reconsider t1 =t as transition of CPNT2 by Q0,CAS2,XBOOLE_0:def 5;
      not t1 is outbound by Q1;
      then {t1}*' <> {} by Def7; then
Q2: ex g be set st g in {t1}*' by XBOOLE_0:def 1;
      {t1}*' c= {t}*' by LM6,LM6S1,LM6S2,LM6S3,LM6S4; then
      not (ex w be transition of CPNT12 st t=w & w is outbound ) by Def7,Q2;
      hence not x in Outbds(CPNT12);
    end;
      suppose CAS3:t in dom RR3;
      t in dom O12 by P1,FUNCT_2:def 1,CAS3; then
      consider s be set such that
FF: [t,s] in O12 by RELAT_1:def 4;
      reconsider s as place of CPNT2 by FF,ZFMISC_1:106;
A5:  O12 c= E31 \/ E32 by XBOOLE_1:7;
      E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7; then
      O12 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5; then
      reconsider f= [t,s] as T-S_arc of CPNT12 by FF;
A4: s in the Places of CPNT2;
A31: the Places of CPNT2
      c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
      t in {t} & f=[t,s] by TARSKI:def 1; then
      s in {t}*' by A4,A31; then
      not (ex w be transition of CPNT12 st t=w & w is outbound) by Def7;
      hence not x in Outbds(CPNT12);
   end;
      suppose CAS4:t in dom RR4;
      t in dom O21 by P1,FUNCT_2:def 1,CAS4;
      then consider s be set such that
FF: [t,s] in O21 by RELAT_1:def 4;
      reconsider s as place of CPNT1 by FF,ZFMISC_1:106;
A5: O21 c= E31 \/ E32 by XBOOLE_1:7;
      E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
      then O21 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5;
      then reconsider f= [t,s]  as T-S_arc of CPNT12 by FF;
A4: s in the Places of CPNT1;
A31:the Places of CPNT1
      c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
      t in {t} & f=[t,s] by TARSKI:def 1;
      then s in {t}*' by A31,A4; then
      not (ex w be transition of CPNT12 st t=w & w is outbound) by Def7;
      hence not x in Outbds(CPNT12);
    end;
  end;
  hence x in (the Transitions of CPNT12) \ Outbds(CPNT12)
    by ASD,S10,XBOOLE_0:def 5;
  end;
  then CPNT12 is Colored-PT-net-like by SS1,Def4;
  hence thesis by P1,P2;
end;
uniqueness
  proof
    let CA,CB be strict Colored-PT-net;
    assume
AS1: ex q12A,q21A be Function,
    O12A be Function of Outbds(CPNT1), the Places of CPNT2,
    O21A be Function of Outbds(CPNT2), the Places of CPNT1 st
    O=[O12A,O21A]
    &dom q12A=Outbds(CPNT1) & dom q21A=Outbds(CPNT2) &
    ( for t01 be transition of CPNT1 st t01 is outbound holds
    q12A.t01 is Function of
    thin_cylinders (the ColoredSet of CPNT1, *'{t01}),
    thin_cylinders (the ColoredSet of CPNT1, Im(O12A,t01) ) ) &
    (for t02 be transition of CPNT2 st t02 is outbound holds
    q21A.t02 is Function of
    thin_cylinders ( the ColoredSet of CPNT2, *'{t02}),
    thin_cylinders ( the ColoredSet of CPNT2, Im(O21A,t02)
     ) ) & q=[q12A,q21A]
    & the Places of CA = (the Places of CPNT1) \/ (the Places of CPNT2) &
    the Transitions of CA =
    (the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
    the S-T_Arcs of CA =
    (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
    the T-S_Arcs of CA =
    (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12A \/ O21A &
    the ColoredSet of CA = (the ColoredSet of CPNT1)
    \/ (the ColoredSet of CPNT2) &
    the firing-rule of CA =
    (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12A +* q21A;
    assume
BS1: ex q12B,q21B be Function,
    O12B be Function of Outbds(CPNT1), the Places of CPNT2,
    O21B be Function of Outbds(CPNT2), the Places of CPNT1 st
    O=[O12B,O21B]
    & dom q12B=Outbds(CPNT1) & dom q21B=Outbds(CPNT2) &
    ( for t01 be transition of CPNT1 st t01 is outbound holds
    q12B.t01 is Function of
    thin_cylinders ( the ColoredSet of CPNT1, *'{t01}),
    thin_cylinders ( the ColoredSet of CPNT1, Im(O12B,t01) ) ) &
    ( for t02 be transition of CPNT2 st t02 is outbound holds
    q21B.t02 is Function of
    thin_cylinders ( the ColoredSet of CPNT2, *'{t02}),
    thin_cylinders ( the ColoredSet of CPNT2, Im(O21B,t02)
     ) ) & q=[q12B,q21B]
    & the Places of CB = (the Places of CPNT1) \/ (the Places of CPNT2) &
    the Transitions of CB =
    (the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
    the S-T_Arcs of CB = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2)
    &
    the T-S_Arcs of CB = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
    \/ O12B \/ O21B &
    the ColoredSet of CB = (the ColoredSet of CPNT1)
    \/ (the ColoredSet of CPNT2) &
    the firing-rule of CB =
    (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12B +* q21B;
    consider q12A,q21A be Function,
    O12A be Function of Outbds(CPNT1), the Places of CPNT2,
    O21A be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: O=[O12A,O21A] & dom q12A=Outbds(CPNT1)
    & dom q21A=Outbds(CPNT2) &
    ( for t01 be transition of CPNT1 st t01 is outbound holds
    q12A.t01 is Function of
    thin_cylinders ( the ColoredSet of CPNT1, *'{t01}),
    thin_cylinders ( the ColoredSet of CPNT1, Im(O12A,t01) ) ) &
    ( for t02 be transition of CPNT2 st t02 is outbound holds
    q21A.t02 is Function of
    thin_cylinders ( the ColoredSet of CPNT2, *'{t02}),
    thin_cylinders ( the ColoredSet of CPNT2, Im(O21A,t02)) )
    & q=[q12A,q21A]
    & the Places of CA = (the Places of CPNT1) \/ (the Places of CPNT2) &
    the Transitions of CA =
    (the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
    the S-T_Arcs of CA =
    (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
    the T-S_Arcs of CA =
    (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12A \/O21A &
    the ColoredSet of CA = (the ColoredSet of CPNT1)
    \/ (the ColoredSet of CPNT2) &
    the firing-rule of CA =
    (the firing-rule of CPNT1) +* (the firing-rule of CPNT2)
    +* q12A +* q21A by AS1;
    consider q12B,q21B be Function,
    O12B be Function of Outbds(CPNT1), the Places of CPNT2,
    O21B be Function of Outbds(CPNT2), the Places of CPNT1 such that
P2: O=[O12B,O21B] & dom q12B=Outbds(CPNT1)
    & dom q21B=Outbds(CPNT2) &
    ( for t01 be transition of CPNT1 st t01 is outbound holds
    q12B.t01 is Function of
    thin_cylinders ( the ColoredSet of CPNT1, *'{t01}),
    thin_cylinders ( the ColoredSet of CPNT1, Im(O12B,t01)) ) &
    ( for t02 be transition of CPNT2 st t02 is outbound holds
    q21B.t02 is Function of
    thin_cylinders ( the ColoredSet of CPNT2, *'{t02}),
    thin_cylinders ( the ColoredSet of CPNT2, Im(O21B,t02)) ) & q=[q12B,q21B]
    & the Places of CB = (the Places of CPNT1) \/ (the Places of CPNT2) &
    the Transitions of CB =
    (the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
    the S-T_Arcs of CB =
    (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
    the T-S_Arcs of CB =
    (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12B \/O21B &
    the ColoredSet of CB = (the ColoredSet of CPNT1)
    \/ (the ColoredSet of CPNT2) &
    the firing-rule of CB =
    (the firing-rule of CPNT1) +* (the firing-rule of CPNT2)
    +* q12B +* q21B by BS1;
P3: q12A=q12B & q21A =q21B by P1,P2,ZFMISC_1:33;
    O12A=O12B & O21A =O21B by P1,P2,ZFMISC_1:33;
    hence thesis by P1,P2,P3;
  end;
end;