let X be non empty set ; :: thesis: for f being FinSequence of X holds PairF f is oriented Chain of PGraph X
let f be FinSequence of X; :: thesis: PairF f is oriented Chain of PGraph X

A1: now

per cases ( len f >= 1 or len f < 1 ) ;

case len f >= 1 ; :: thesis: PairF f is Chain of PGraph X

then ((len f) - 1) + 1 = ((len f) -' 1) + 1 by XREAL_1:235;
then A2: len f = (len (PairF f)) + 1 by Def2;
A3: for n being Element of NAT st 1 <= n & n <= len f holds
f . n in the carrier of (PGraph X)

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len f implies f . n in the carrier of (PGraph X) )
assume ( 1 <= n & n <= len f ) ; :: thesis: f . n in the carrier of (PGraph X)
then n in dom f by FINSEQ_3:27;
then f . n in rng f by FUNCT_1:def 5;
hence f . n in the carrier of (PGraph X) ; :: thesis: verum

end;

for n being Element of NAT st 1 <= n & n <= len (PairF f) holds
ex x', y' being Element of the carrier of (PGraph X) st
( x' = f . n & y' = f . (n + 1) & (PairF f) . n joins x',y' )

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (PairF f) implies ex x', y' being Element of the carrier of (PGraph X) st
( x' = f . n & y' = f . (n + 1) & (PairF f) . n joins x',y' ) )
assume A4: ( 1 <= n & n <= len (PairF f) ) ; :: thesis: ex x', y' being Element of the carrier of (PGraph X) st
( x' = f . n & y' = f . (n + 1) & (PairF f) . n joins x',y' )
A5: len (PairF f) = (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by A4, XXREAL_0:2;
then A6: (len f) -' 1 = (len f) - 1 by NAT_D:39;
(len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
then A7: n < len f by A4, A5, A6, XXREAL_0:2;
then n in dom f by A4, FINSEQ_3:27;
then A8: f . n in rng f by FUNCT_1:def 5;
A9: 1 < n + 1 by A4, NAT_1:13;
n + 1 <= len f by A7, NAT_1:13;
then n + 1 in dom f by A9, FINSEQ_3:27;
then A10: f . (n + 1) in rng f by FUNCT_1:def 5;
then reconsider a = f . n, b = f . (n + 1) as Element of the carrier of (PGraph X) by A8;
A11: (pr1 X,X) . (f . n),(f . (n + 1)) = f . n by A8, A10, FUNCT_3:def 5;
(pr2 X,X) . (f . n),(f . (n + 1)) = f . (n + 1) by A8, A10, FUNCT_3:def 6;
then ( the Source of (PGraph X) . ((PairF f) . n) = a & the Target of (PGraph X) . ((PairF f) . n) = b ) by A4, A7, A11, Def2;
then (PairF f) . n joins a,b by GRAPH_1:def 10;
hence ex x', y' being Element of the carrier of (PGraph X) st
( x' = f . n & y' = f . (n + 1) & (PairF f) . n joins x',y' ) ; :: thesis: verum

end;

then ( ( for n being Element of NAT st 1 <= n & n <= len (PairF f) holds
(PairF f) . n in the carrier' of (PGraph X) ) & ex p being FinSequence st
( len p = (len (PairF f)) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of (PGraph X) ) & ( for n being Element of NAT st 1 <= n & n <= len (PairF f) holds
ex x', y' being Element of the carrier of (PGraph X) st
( x' = p . n & y' = p . (n + 1) & (PairF f) . n joins x',y' ) ) ) ) by A2, A3, Th9;
hence PairF f is Chain of PGraph X by GRAPH_1:def 12; :: thesis: verum

end;

case len f < 1 ; :: thesis: PairF f is oriented Chain of PGraph X

then (len f) + 1 <= 1 by NAT_1:13;
then ((len f) + 1) - 1 <= 1 - 1 by XREAL_1:11;
then A12: len f = 0 ;
0 - 1 < 0 ;
then (len f) -' 1 = 0 by A12, XREAL_0:def 2;
then len (PairF f) = 0 by Def2;
then PairF f = {} ;
hence PairF f is oriented Chain of PGraph X by GRAPH_1:14; :: thesis: verum

end;

end;

end;

for n being Element of NAT st 1 <= n & n < len (PairF f) holds
the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len (PairF f) implies the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n) )
assume A13: ( 1 <= n & n < len (PairF f) ) ; :: thesis: the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)
then A14: n + 1 <= len (PairF f) by NAT_1:13;
A15: len (PairF f) = (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by A13, XXREAL_0:2;
then A16: (len f) -' 1 = (len f) - 1 by NAT_D:39;
A17: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
then A18: n < len f by A13, A15, A16, XXREAL_0:2;
A19: n + 1 < len f by A14, A15, A16, A17, XXREAL_0:2;
n in dom f by A13, A18, FINSEQ_3:27;
then A20: f . n in rng f by FUNCT_1:def 5;
A21: 1 < n + 1 by A13, NAT_1:13;
n + 1 <= len f by A18, NAT_1:13;
then n + 1 in dom f by A21, FINSEQ_3:27;
then A22: f . (n + 1) in rng f by FUNCT_1:def 5;
then reconsider a = f . n, b = f . (n + 1) as Element of the carrier of (PGraph X) by A20;
A23: (pr1 X,X) . (f . n),(f . (n + 1)) = f . n by A20, A22, FUNCT_3:def 5;
(pr2 X,X) . (f . n),(f . (n + 1)) = f . (n + 1) by A20, A22, FUNCT_3:def 6;
then A24: ( the Source of (PGraph X) . ((PairF f) . n) = a & the Target of (PGraph X) . ((PairF f) . n) = b ) by A13, A18, A23, Def2;
n + 1 in dom f by A19, A21, FINSEQ_3:27;
then A25: f . (n + 1) in rng f by FUNCT_1:def 5;
A26: 1 < (n + 1) + 1 by A21, NAT_1:13;
(n + 1) + 1 <= len f by A19, NAT_1:13;
then (n + 1) + 1 in dom f by A26, FINSEQ_3:27;
then f . ((n + 1) + 1) in rng f by FUNCT_1:def 5;
then (pr1 X,X) . (f . (n + 1)),(f . ((n + 1) + 1)) = f . (n + 1) by A25, FUNCT_3:def 5;
hence the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n) by A19, A21, A24, Def2; :: thesis: verum

end;

hence PairF f is oriented Chain of PGraph X by A1, GRAPH_1:def 13; :: thesis: verum