let X be non empty set ; :: thesis: for f being FinSequence of X holds PairF f is FinSequence of the carrier' of (PGraph X)

let f be FinSequence of X; :: thesis: PairF f is FinSequence of the carrier' of (PGraph X)

rng (PairF f) c= [:X,X:]

let f be FinSequence of X; :: thesis: PairF f is FinSequence of the carrier' of (PGraph X)

rng (PairF f) c= [:X,X:]

proof

hence
PairF f is FinSequence of the carrier' of (PGraph X)
by FINSEQ_1:def 4; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (PairF f) or y in [:X,X:] )

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

assume y in rng (PairF f) ; :: thesis: y in [:X,X:]

then consider x being object such that

A2: x in dom (PairF f) and

A3: y = (PairF f) . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A2;

A4: x in Seg (len (PairF f)) by A2, FINSEQ_1:def 3;

then A5: 1 <= n by FINSEQ_1:1;

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

A7: n <= len (PairF f) by A4, FINSEQ_1:1;

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

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

then A8: n < len f by A7, A6, A1, XXREAL_0:2;

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

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

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

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

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

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

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

hence y in [:X,X:] by A3, A11, A10, ZFMISC_1:def 2; :: thesis: verum

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

assume y in rng (PairF f) ; :: thesis: y in [:X,X:]

then consider x being object such that

A2: x in dom (PairF f) and

A3: y = (PairF f) . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A2;

A4: x in Seg (len (PairF f)) by A2, FINSEQ_1:def 3;

then A5: 1 <= n by FINSEQ_1:1;

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

A7: n <= len (PairF f) by A4, FINSEQ_1:1;

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

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

then A8: n < len f by A7, A6, A1, XXREAL_0:2;

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

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

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

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

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

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

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

hence y in [:X,X:] by A3, A11, A10, ZFMISC_1:def 2; :: thesis: verum