let XP1, XP2 be strict Colored-PT-net; ( 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 )
; ( 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 )
; 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
X3: dom T1 =
I
by PARTFUN1:def 2
.=
dom T2
by PARTFUN1:def 2
;
A2:
T1 = T2
X5: dom ST1 =
I
by PARTFUN1:def 2
.=
dom ST2
by PARTFUN1:def 2
;
A3:
ST1 = ST2
X7: dom TS1 =
I
by PARTFUN1:def 2
.=
dom TS2
by PARTFUN1:def 2
;
A4:
TS1 = TS2
X9: dom CS1 =
I
by PARTFUN1:def 2
.=
dom CS2
by PARTFUN1:def 2
;
A5:
CS1 = CS2
X11: dom F1 =
I
by PARTFUN1:def 2
.=
dom F2
by PARTFUN1:def 2
;
F1 = F2
hence
XP1 = XP2
by A1, A2, A3, A4, A5, D1, D2; verum