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