let B1, B2 be marking of PTN; :: thesis: ( ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) & ( not Q = {} & ex M being FinSequence of nat_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 nat_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 ) ; :: thesis: ( not Q = {} & ex M being FinSequence of nat_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 nat_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 <> {} ; :: thesis: ( for M being FinSequence of nat_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 nat_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 nat_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)) ; :: thesis: ( for M being FinSequence of nat_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 ;
given M2 being FinSequence of nat_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)) ; :: thesis: B1 = B2
defpred S1[ Nat] means ( \$1 in Seg (len Q) implies M1 /. \$1 = M2 /. \$1 );
A39: now :: thesis: for j being Nat st S1[j] holds
S1[j + 1]
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A40: S1[j] ; :: thesis: S1[j + 1]
now :: thesis: ( j + 1 in Seg (len Q) implies M1 /. (j + 1) = M2 /. (j + 1) )
assume A41: j + 1 in Seg (len Q) ; :: thesis: M1 /. (j + 1) = M2 /. (j + 1)
per cases ( j = 0 or j <> 0 ) ;
suppose j = 0 ; :: thesis: M1 /. (j + 1) = M2 /. (j + 1)
hence M1 /. (j + 1) = M2 /. (j + 1) by ; :: thesis: verum
end;
suppose A42: j <> 0 ; :: thesis: M1 /. (j + 1) = M2 /. (j + 1)
( j + 1 <= len Q & j < j + 1 ) by ;
then A44: j < len Q by XXREAL_0:2;
1 <= j by ;
then B2: j in dom Q by ;
thus M1 /. (j + 1) = Firing ((Q /. (j + 1)),(M1 /. j)) by
.= M2 /. (j + 1) by ; :: thesis: verum
end;
end;
end;
hence S1[j + 1] ; :: thesis: verum
end;
A45: S1[ 0 ] by FINSEQ_1:1;
A46: for j being Nat holds S1[j] from
now :: thesis: for j being Nat st j in dom M1 holds
M1 . j = M2 . j
let j be Nat; :: thesis: ( j in dom M1 implies M1 . j = M2 . j )
assume A47: j in dom M1 ; :: thesis: M1 . j = M2 . j
then A48: j in dom M2 by ;
thus M1 . j = M1 /. j by
.= M2 /. j by
.= M2 . j by ; :: thesis: verum
end;
hence B1 = B2 by ; :: thesis: verum