let i be Nat; :: thesis: for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & i in dom dct holds
i mod 2 = 1
let Dftn be Petri With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & i in dom dct holds
i mod 2 = 1
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in places_of dct & i in dom dct implies i mod 2 = 1 )
assume that
T2: dct . i in places_of dct and
T4: i in dom dct ; :: thesis: i mod 2 = 1
consider p being place of Dftn such that
T3: ( p = dct . i & p in rng dct ) by T2;
E1: ( 1 <= i & i <= len dct ) by T4, FINSEQ_3:25;
E41: ( i = len dct or i < len dct ) by XXREAL_0:1, E1;
i mod 2 = 1

proof

assume E6: i mod 2 <> 1 ; :: thesis: contradiction
reconsider i1 = i - 1 as Element of NAT by NAT_1:21, T4, FINSEQ_3:25;

now :: thesis: not i1 mod 2 = 0

assume i1 mod 2 = 0 ; :: thesis: contradiction
then (i1 + 1) mod 2 = 1 by NAT_D:16;
hence contradiction by E6; :: thesis: verum

end;

then i1 mod 2 = 1 by NAT_D:12;
then [(dct . i1),(dct . (i1 + 1))] in the S-T_Arcs of Dftn by E6, E41, Def5;
then dct . (i1 + 1) in the carrier' of Dftn by ZFMISC_1:87;
hence contradiction by XBOOLE_0:3, NET_1:def 2, T3; :: thesis: verum

end;

hence i mod 2 = 1 ; :: thesis: verum