let B1, B2 be Boolean_marking of PTN; ( ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & B1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & B2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies B1 = B2 ) )
thus
( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 )
; ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & B1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & B2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies B1 = B2 )
assume
Q <> {}
; ( for M being FinSequence of Bool_marks_of PTN holds
( not len Q = len M or not B1 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or for M being FinSequence of Bool_marks_of PTN holds
( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 )
given M1 being FinSequence of Bool_marks_of PTN such that A30:
len Q = len M1
and
A31:
B1 = M1 /. (len M1)
and
A32:
M1 /. 1 = Firing ((Q /. 1),M0)
and
A33:
for i being Nat st i < len Q & i > 0 holds
M1 /. (i + 1) = Firing ((Q /. (i + 1)),(M1 /. i))
; ( for M being FinSequence of Bool_marks_of PTN holds
( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 )
A34:
dom M1 = Seg (len Q)
by A30, FINSEQ_1:def 3;
given M2 being FinSequence of Bool_marks_of PTN such that A35:
len Q = len M2
and
A36:
B2 = M2 /. (len M2)
and
A37:
M2 /. 1 = Firing ((Q /. 1),M0)
and
A38:
for i being Nat st i < len Q & i > 0 holds
M2 /. (i + 1) = Firing ((Q /. (i + 1)),(M2 /. i))
; B1 = B2
defpred S1[ Nat] means ( $1 in Seg (len Q) implies M1 /. $1 = M2 /. $1 );
A39:
now for j being Nat st S1[j] holds
S1[j + 1]end;
A45:
S1[ 0 ]
by FINSEQ_1:1;
A46:
for j being Nat holds S1[j]
from NAT_1:sch 2(A45, A39);
hence
B1 = B2
by A30, A31, A35, A36, FINSEQ_2:9; verum