let P be set ; :: thesis:
let N be Petri_net of P; :: thesis:
let C be firing-sequence of N; :: thesis:
defpred S₁[ Nat] means for F being Function-yielding FinSequence st len F = $1 & ( for i being Nat st i in dom F holds
ex t being transition of P st F . i = fire t ) holds
( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) );
A1: S₁[ 0 ]

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A3: for G being Function-yielding FinSequence st len G = k & ( for i being Nat st i in dom G holds
ex t being transition of P st G . i = fire t ) holds
( dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ; :: thesis:
let F be Function-yielding FinSequence; :: thesis:
assume that
A4: len F = k + 1 and
A5: for i being Nat st i in dom F holds
ex t being transition of P st F . i = fire t ; :: thesis:
consider G being FinSequence, x being set such that
A6: F = G ^ <*x*> and
A7: len G = k by A4, TREES_2:3;
reconsider G = G as Function-yielding FinSequence by A6, FUNCT_7:23;
0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom F by A4, FINSEQ_3:25;
then consider t being transition of P such that
A8: F . (k + 1) = fire t by A5;
x = F . (k + 1) by A6, A7, FINSEQ_1:42;
then A9: compose (F,(Funcs (P,NAT))) = (fire t) * (compose (G,(Funcs (P,NAT)))) by A6, A8, FUNCT_7:41;
A10: dom (fire t) = Funcs (P,NAT) by Def8;
A11: rng (fire t) c= Funcs (P,NAT) by Th20;
A12: for i being Nat st i in dom G holds
ex t being transition of P st G . i = fire t

end;

end;

A17: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
consider F being Function-yielding FinSequence such that
A18: fire C = compose (F,(Funcs (P,NAT))) and
A19: len F = len C and
A20: for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) by Def10;
for i being Nat st i in dom F holds
ex t being transition of P st F . i = fire t

end;