let B1, B2 be marking of PTN; :: thesis:
thus ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) ; :: thesis:
assume Q <> {} ; :: thesis:
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:
A34: dom M1 = Seg (len Q) by A30, FINSEQ_1:def 3;
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:
defpred S₁[ Nat] means ( $1 in Seg (len Q) implies M1 /. $1 = M2 /. $1 );

A39: now :: thesis:

let j be Nat; :: thesis:
assume A40: S₁[j] ; :: thesis:

now :: thesis:

assume A41: j + 1 in Seg (len Q) ; :: thesis:

per cases ;

suppose j = 0 ; :: thesis:

hence M1 /. (j + 1) = M2 /. (j + 1) by A32, A37; :: thesis:

end;

suppose A42: j <> 0 ; :: thesis:

( j + 1 <= len Q & j < j + 1 ) by A41, FINSEQ_1:1, XREAL_1:29;
then A44: j < len Q by XXREAL_0:2;
1 <= j by A42, NAT_1:14;
then B2: j in dom Q by A44, FINSEQ_3:25;
thus M1 /. (j + 1) = Firing ((Q /. (j + 1)),(M1 /. j)) by A33, A44, A42
.= M2 /. (j + 1) by A38, A44, A42, A40, FINSEQ_1:def 3, B2 ; :: thesis:

end;

end;

end;

hence S₁[j + 1] ; :: thesis:

end;

A45: S₁[ 0 ] by FINSEQ_1:1;
A46: for j being Nat holds S₁[j] from NAT_1:sch 2(A45, A39);

now :: thesis:

let j be Nat; :: thesis:
assume A47: j in dom M1 ; :: thesis:
then A48: j in dom M2 by A35, A34, FINSEQ_1:def 3;
thus M1 . j = M1 /. j by A47, PARTFUN1:def 6
.= M2 /. j by A46, A34, A47
.= M2 . j by A48, PARTFUN1:def 6 ; :: thesis:

end;

hence B1 = B2 by A30, A31, A35, A36, FINSEQ_2:9; :: thesis: