let P be set ; :: thesis: for N being Petri_net of P
for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let N be Petri_net of P; :: thesis: for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let C be firing-sequence of N; :: thesis: ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
defpred S1[ 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: S1[ 0 ]
proof
let F be Function-yielding FinSequence; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds
ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

assume len F = 0 ; :: thesis: ( ex i being Nat st
( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

then F = {} ;
then compose (F,(Funcs (P,NAT))) = id (Funcs (P,NAT)) by FUNCT_7:39;
hence ( ex i being Nat st
( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ) ; :: thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
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: S1[k + 1]
let F be Function-yielding FinSequence; :: thesis: ( len F = k + 1 & ( for i being Nat st i in dom F holds
ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

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: ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) )
consider G being FinSequence, x being set such that
A6: F = G ^ <*x*> and
A7: len G = k by ;
reconsider G = G as Function-yielding FinSequence by ;
0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom F by ;
then consider t being transition of P such that
A8: F . (k + 1) = fire t by A5;
x = F . (k + 1) by ;
then A9: compose (F,(Funcs (P,NAT))) = (fire t) * (compose (G,(Funcs (P,NAT)))) by ;
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
proof
let i be Nat; :: thesis: ( i in dom G implies ex t being transition of P st G . i = fire t )
A13: dom G c= dom F by ;
assume A14: i in dom G ; :: thesis: ex t being transition of P st G . i = fire t
then G . i = F . i by ;
hence ex t being transition of P st G . i = fire t by A5, A13, A14; :: thesis: verum
end;
then A15: dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) by A3, A7;
A16: rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) by A3, A7, A12;
rng (compose (F,(Funcs (P,NAT)))) c= rng (fire t) by ;
hence ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) by ; :: thesis: verum
end;
A17: for k being Nat holds S1[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
proof
let i be Nat; :: thesis: ( i in dom F implies ex t being transition of P st F . i = fire t )
assume A21: i in dom F ; :: thesis: ex t being transition of P st F . i = fire t
A22: dom F = Seg (len F) by FINSEQ_1:def 3;
A23: dom C = Seg (len C) by FINSEQ_1:def 3;
reconsider t = C /. i as Element of N ;
take t ; :: thesis: F . i = fire t
thus F . i = fire t by A19, A20, A21, A22, A23; :: thesis: verum
end;
hence ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) ) by ; :: thesis: verum