let X be non empty set ; 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; 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; ( 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)
; (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; verum