let X be non empty set ; :: thesis: for n being Nat

for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds

(PairF f) . n in the carrier' of (PGraph X)

let n be Nat; :: thesis: for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds

(PairF f) . n in the carrier' of (PGraph X)

let f be FinSequence of X; :: thesis: ( 1 <= n & n <= len (PairF f) implies (PairF f) . n in the carrier' of (PGraph X) )

assume that

A1: 1 <= n and

A2: n <= len (PairF f) ; :: thesis: (PairF f) . n in the carrier' of (PGraph X)

A3: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;

A4: len (PairF f) = (len f) -' 1 by Def2;

then 1 <= (len f) -' 1 by A1, A2, XXREAL_0:2;

then (len f) -' 1 = (len f) - 1 by NAT_D:39;

then A5: n < len f by A2, A4, A3, XXREAL_0:2;

then A6: n + 1 <= len f by NAT_1:13;

1 < n + 1 by A1, NAT_1:13;

then n + 1 in dom f by A6, FINSEQ_3:25;

then A7: f . (n + 1) in rng f by FUNCT_1:def 3;

n in dom f by A1, A5, FINSEQ_3:25;

then A8: f . n in rng f by FUNCT_1:def 3;

(PairF f) . n = [(f . n),(f . (n + 1))] by A1, A5, Def2;

hence (PairF f) . n in the carrier' of (PGraph X) by A8, A7, ZFMISC_1:def 2; :: thesis: verum

for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds

(PairF f) . n in the carrier' of (PGraph X)

let n be Nat; :: thesis: for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds

(PairF f) . n in the carrier' of (PGraph X)

let f be FinSequence of X; :: thesis: ( 1 <= n & n <= len (PairF f) implies (PairF f) . n in the carrier' of (PGraph X) )

assume that

A1: 1 <= n and

A2: n <= len (PairF f) ; :: thesis: (PairF f) . n in the carrier' of (PGraph X)

A3: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;

A4: len (PairF f) = (len f) -' 1 by Def2;

then 1 <= (len f) -' 1 by A1, A2, XXREAL_0:2;

then (len f) -' 1 = (len f) - 1 by NAT_D:39;

then A5: n < len f by A2, A4, A3, XXREAL_0:2;

then A6: n + 1 <= len f by NAT_1:13;

1 < n + 1 by A1, NAT_1:13;

then n + 1 in dom f by A6, FINSEQ_3:25;

then A7: f . (n + 1) in rng f by FUNCT_1:def 3;

n in dom f by A1, A5, FINSEQ_3:25;

then A8: f . n in rng f by FUNCT_1:def 3;

(PairF f) . n = [(f . n),(f . (n + 1))] by A1, A5, Def2;

hence (PairF f) . n in the carrier' of (PGraph X) by A8, A7, ZFMISC_1:def 2; :: thesis: verum