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 :: thesis: ( ( len f >= 1 & PairF f is Chain of PGraph X ) or ( len f < 1 & PairF f is oriented Chain of PGraph X ) )
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:233;
then A2: len f = (len ()) + 1 by Def2;
A3: for n being Nat st 1 <= n & n <= len f holds
f . n in the carrier of ()
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len f implies f . n in the carrier of () )
assume ( 1 <= n & n <= len f ) ; :: thesis: f . n in the carrier of ()
then n in dom f by FINSEQ_3:25;
then f . n in rng f by FUNCT_1:def 3;
hence f . n in the carrier of () ; :: thesis: verum
end;
A4: for n being Nat st 1 <= n & n <= len () holds
ex x9, y9 being Element of () st
( x9 = f . n & y9 = f . (n + 1) & () . n joins x9,y9 )
proof
A5: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
let n be Nat; :: thesis: ( 1 <= n & n <= len () implies ex x9, y9 being Element of () st
( x9 = f . n & y9 = f . (n + 1) & () . n joins x9,y9 ) )

assume that
A6: 1 <= n and
A7: n <= len () ; :: thesis: ex x9, y9 being Element of () st
( x9 = f . n & y9 = f . (n + 1) & () . n joins x9,y9 )

A8: 1 < n + 1 by ;
A9: len () = (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by ;
then (len f) -' 1 = (len f) - 1 by NAT_D:39;
then A10: n < len f by ;
then n + 1 <= len f by NAT_1:13;
then n + 1 in dom f by ;
then A11: f . (n + 1) in rng f by FUNCT_1:def 3;
n in dom f by ;
then A12: f . n in rng f by FUNCT_1:def 3;
then reconsider a = f . n, b = f . (n + 1) as Element of () by A11;
(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by ;
then A13: the Target of () . (() . n) = b by ;
(pr1 (X,X)) . ((f . n),(f . (n + 1))) = f . n by ;
then the Source of () . (() . n) = a by ;
then (PairF f) . n joins a,b by ;
hence ex x9, y9 being Element of () st
( x9 = f . n & y9 = f . (n + 1) & () . n joins x9,y9 ) ; :: thesis: verum
end;
for n being Nat st 1 <= n & n <= len () holds
() . n in the carrier' of () by Th5;
hence PairF f is Chain of PGraph X by ; :: 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:9;
then A14: len f = 0 ;
0 - 1 < 0 ;
then (len f) -' 1 = 0 by ;
then len () = 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 Nat st 1 <= n & n < len () holds
the Source of () . (() . (n + 1)) = the Target of () . (() . n)
proof
A15: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
let n be Nat; :: thesis: ( 1 <= n & n < len () implies the Source of () . (() . (n + 1)) = the Target of () . (() . n) )
assume that
A16: 1 <= n and
A17: n < len () ; :: thesis: the Source of () . (() . (n + 1)) = the Target of () . (() . n)
A18: len () = (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by ;
then A19: (len f) -' 1 = (len f) - 1 by NAT_D:39;
then A20: n < len f by ;
then n in dom f by ;
then A21: f . n in rng f by FUNCT_1:def 3;
n + 1 <= len () by ;
then A22: n + 1 < len f by ;
then A23: (n + 1) + 1 <= len f by NAT_1:13;
A24: 1 < n + 1 by ;
then 1 < (n + 1) + 1 by NAT_1:13;
then (n + 1) + 1 in dom f by ;
then A25: f . ((n + 1) + 1) in rng f by FUNCT_1:def 3;
n + 1 <= len f by ;
then n + 1 in dom f by ;
then A26: f . (n + 1) in rng f by FUNCT_1:def 3;
then reconsider b = f . (n + 1) as Element of () ;
(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by ;
then A27: the Target of () . (() . n) = b by ;
n + 1 in dom f by ;
then f . (n + 1) in rng f by FUNCT_1:def 3;
then (pr1 (X,X)) . ((f . (n + 1)),(f . ((n + 1) + 1))) = f . (n + 1) by ;
hence the Source of () . (() . (n + 1)) = the Target of () . (() . n) by ; :: thesis: verum
end;
hence PairF f is oriented Chain of PGraph X by ; :: thesis: verum