let X be non empty set ; :: thesis: for n being Element of 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 Element of 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 A1: ( 1 <= n & n <= len (PairF f) ) ; :: thesis: (PairF f) . n in the carrier' of (PGraph X)
A2: len (PairF f) = (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by A1, XXREAL_0:2;
then A3: (len f) -' 1 = (len f) - 1 by NAT_D:39;
(len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
then A4: n < len f by A1, A2, A3, XXREAL_0:2;
then A5: (PairF f) . n = [(f . n),(f . (n + 1))] by A1, Def2;
n in dom f by A1, A4, FINSEQ_3:27;
then A6: f . n in rng f by FUNCT_1:def 5;
A7: 1 < n + 1 by A1, NAT_1:13;
n + 1 <= len f by A4, NAT_1:13;
then n + 1 in dom f by A7, FINSEQ_3:27;
then f . (n + 1) in rng f by FUNCT_1:def 5;
hence (PairF f) . n in the carrier' of (PGraph X) by A5, A6, ZFMISC_1:def 2; :: thesis: verum