let XP1, XP2 be strict Colored-PT-net; :: thesis: ( ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP1 = union (rng P) & the carrier' of XP1 = union (rng T) & the S-T_Arcs of XP1 = union (rng ST) & the T-S_Arcs of XP1 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS) & the firing-rule of XP1 = UF +* UQ ) & ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP2 = union (rng P) & the carrier' of XP2 = union (rng T) & the S-T_Arcs of XP2 = union (rng ST) & the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS) & the firing-rule of XP2 = UF +* UQ ) implies XP1 = XP2 )

assume AS1: ex P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I ex UF1, UQ1 being Function st

( ( for i being Element of I holds

( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) ; :: thesis: ( for P, T, ST, TS, CS, F being ManySortedSet of I

for UF, UQ being Function holds

( ex i being Element of I st

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) implies not F . i = the firing-rule of (CPNT . i) ) or not UF = union (rng F) or not UQ = union (rng q) or not the carrier of XP2 = union (rng P) or not the carrier' of XP2 = union (rng T) or not the S-T_Arcs of XP2 = union (rng ST) or not the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) or not the ColoredSet of XP2 = union (rng CS) or not the firing-rule of XP2 = UF +* UQ ) or XP1 = XP2 )

assume AS2: ex P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I ex UF2, UQ2 being Function st

( ( for i being Element of I holds

( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) ; :: thesis: XP1 = XP2

consider P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I, UF1, UQ1 being Function such that

D1: ( ( for i being Element of I holds

( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) by AS1;

consider P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I, UF2, UQ2 being Function such that

D2: ( ( for i being Element of I holds

( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) by AS2;

X1: dom P1 = I by PARTFUN1:def 2

.= dom P2 by PARTFUN1:def 2 ;

A1: P1 = P2

.= dom T2 by PARTFUN1:def 2 ;

A2: T1 = T2

.= dom ST2 by PARTFUN1:def 2 ;

A3: ST1 = ST2

.= dom TS2 by PARTFUN1:def 2 ;

A4: TS1 = TS2

.= dom CS2 by PARTFUN1:def 2 ;

A5: CS1 = CS2

.= dom F2 by PARTFUN1:def 2 ;

F1 = F2

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP1 = union (rng P) & the carrier' of XP1 = union (rng T) & the S-T_Arcs of XP1 = union (rng ST) & the T-S_Arcs of XP1 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS) & the firing-rule of XP1 = UF +* UQ ) & ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP2 = union (rng P) & the carrier' of XP2 = union (rng T) & the S-T_Arcs of XP2 = union (rng ST) & the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS) & the firing-rule of XP2 = UF +* UQ ) implies XP1 = XP2 )

assume AS1: ex P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I ex UF1, UQ1 being Function st

( ( for i being Element of I holds

( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) ; :: thesis: ( for P, T, ST, TS, CS, F being ManySortedSet of I

for UF, UQ being Function holds

( ex i being Element of I st

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) implies not F . i = the firing-rule of (CPNT . i) ) or not UF = union (rng F) or not UQ = union (rng q) or not the carrier of XP2 = union (rng P) or not the carrier' of XP2 = union (rng T) or not the S-T_Arcs of XP2 = union (rng ST) or not the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) or not the ColoredSet of XP2 = union (rng CS) or not the firing-rule of XP2 = UF +* UQ ) or XP1 = XP2 )

assume AS2: ex P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I ex UF2, UQ2 being Function st

( ( for i being Element of I holds

( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) ; :: thesis: XP1 = XP2

consider P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I, UF1, UQ1 being Function such that

D1: ( ( for i being Element of I holds

( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) by AS1;

consider P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I, UF2, UQ2 being Function such that

D2: ( ( for i being Element of I holds

( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) by AS2;

X1: dom P1 = I by PARTFUN1:def 2

.= dom P2 by PARTFUN1:def 2 ;

A1: P1 = P2

proof

end;

X3: dom T1 =
I
by PARTFUN1:def 2
now :: thesis: for i being object st i in dom P1 holds

P1 . i = P2 . i

hence
P1 = P2
by FUNCT_1:2, X1; :: thesis: verumP1 . i = P2 . i

let i be object ; :: thesis: ( i in dom P1 implies P1 . i = P2 . i )

assume i in dom P1 ; :: thesis: P1 . i = P2 . i

then reconsider i0 = i as Element of I ;

thus P1 . i = the carrier of (CPNT . i0) by D1

.= P2 . i by D2 ; :: thesis: verum

end;assume i in dom P1 ; :: thesis: P1 . i = P2 . i

then reconsider i0 = i as Element of I ;

thus P1 . i = the carrier of (CPNT . i0) by D1

.= P2 . i by D2 ; :: thesis: verum

.= dom T2 by PARTFUN1:def 2 ;

A2: T1 = T2

proof

end;

X5: dom ST1 =
I
by PARTFUN1:def 2
now :: thesis: for i being object st i in dom T1 holds

T1 . i = T2 . i

hence
T1 = T2
by FUNCT_1:2, X3; :: thesis: verumT1 . i = T2 . i

let i be object ; :: thesis: ( i in dom T1 implies T1 . i = T2 . i )

assume i in dom T1 ; :: thesis: T1 . i = T2 . i

then reconsider i0 = i as Element of I ;

thus T1 . i = the carrier' of (CPNT . i0) by D1

.= T2 . i by D2 ; :: thesis: verum

end;assume i in dom T1 ; :: thesis: T1 . i = T2 . i

then reconsider i0 = i as Element of I ;

thus T1 . i = the carrier' of (CPNT . i0) by D1

.= T2 . i by D2 ; :: thesis: verum

.= dom ST2 by PARTFUN1:def 2 ;

A3: ST1 = ST2

proof

end;

X7: dom TS1 =
I
by PARTFUN1:def 2
now :: thesis: for i being object st i in dom ST1 holds

ST1 . i = ST2 . i

hence
ST1 = ST2
by FUNCT_1:2, X5; :: thesis: verumST1 . i = ST2 . i

let i be object ; :: thesis: ( i in dom ST1 implies ST1 . i = ST2 . i )

assume i in dom ST1 ; :: thesis: ST1 . i = ST2 . i

then reconsider i0 = i as Element of I ;

thus ST1 . i = the S-T_Arcs of (CPNT . i0) by D1

.= ST2 . i by D2 ; :: thesis: verum

end;assume i in dom ST1 ; :: thesis: ST1 . i = ST2 . i

then reconsider i0 = i as Element of I ;

thus ST1 . i = the S-T_Arcs of (CPNT . i0) by D1

.= ST2 . i by D2 ; :: thesis: verum

.= dom TS2 by PARTFUN1:def 2 ;

A4: TS1 = TS2

proof

end;

X9: dom CS1 =
I
by PARTFUN1:def 2
now :: thesis: for i being object st i in dom TS1 holds

TS1 . i = TS2 . i

hence
TS1 = TS2
by FUNCT_1:2, X7; :: thesis: verumTS1 . i = TS2 . i

let i be object ; :: thesis: ( i in dom TS1 implies TS1 . i = TS2 . i )

assume i in dom TS1 ; :: thesis: TS1 . i = TS2 . i

then reconsider i0 = i as Element of I ;

thus TS1 . i = the T-S_Arcs of (CPNT . i0) by D1

.= TS2 . i by D2 ; :: thesis: verum

end;assume i in dom TS1 ; :: thesis: TS1 . i = TS2 . i

then reconsider i0 = i as Element of I ;

thus TS1 . i = the T-S_Arcs of (CPNT . i0) by D1

.= TS2 . i by D2 ; :: thesis: verum

.= dom CS2 by PARTFUN1:def 2 ;

A5: CS1 = CS2

proof

end;

X11: dom F1 =
I
by PARTFUN1:def 2
now :: thesis: for i being object st i in dom CS1 holds

CS1 . i = CS2 . i

hence
CS1 = CS2
by FUNCT_1:2, X9; :: thesis: verumCS1 . i = CS2 . i

let i be object ; :: thesis: ( i in dom CS1 implies CS1 . i = CS2 . i )

assume i in dom CS1 ; :: thesis: CS1 . i = CS2 . i

then reconsider i0 = i as Element of I ;

thus CS1 . i = the ColoredSet of (CPNT . i0) by D1

.= CS2 . i by D2 ; :: thesis: verum

end;assume i in dom CS1 ; :: thesis: CS1 . i = CS2 . i

then reconsider i0 = i as Element of I ;

thus CS1 . i = the ColoredSet of (CPNT . i0) by D1

.= CS2 . i by D2 ; :: thesis: verum

.= dom F2 by PARTFUN1:def 2 ;

F1 = F2

proof

end;

hence
XP1 = XP2
by A1, A2, A3, A4, A5, D1, D2; :: thesis: verumnow :: thesis: for i being object st i in dom F1 holds

F1 . i = F2 . i

hence
F1 = F2
by FUNCT_1:2, X11; :: thesis: verumF1 . i = F2 . i

let i be object ; :: thesis: ( i in dom F1 implies F1 . i = F2 . i )

assume i in dom F1 ; :: thesis: F1 . i = F2 . i

then reconsider i0 = i as Element of I ;

thus F1 . i = the firing-rule of (CPNT . i0) by D1

.= F2 . i by D2 ; :: thesis: verum

end;assume i in dom F1 ; :: thesis: F1 . i = F2 . i

then reconsider i0 = i as Element of I ;

thus F1 . i = the firing-rule of (CPNT . i0) by D1

.= F2 . i by D2 ; :: thesis: verum