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

the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)

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 ) )end;

for n being Nat st 1 <= n & n < len (PairF f) holds per cases
( len f >= 1 or len f < 1 )
;

end;

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 (PairF f)) + 1 by Def2;

A3: for n being Nat st 1 <= n & n <= len f holds

f . n in the carrier of (PGraph X)

ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 )

(PairF f) . n in the carrier' of (PGraph X) by Th5;

hence PairF f is Chain of PGraph X by A2, A3, A4, GRAPH_1:def 14; :: thesis: verum

end;then A2: len f = (len (PairF f)) + 1 by Def2;

A3: for n being Nat st 1 <= n & n <= len f holds

f . n in the carrier of (PGraph X)

proof

A4:
for n being Nat st 1 <= n & n <= len (PairF f) holds
let n be 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:25;

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

hence f . n in the carrier of (PGraph X) ; :: thesis: verum

end;assume ( 1 <= n & n <= len f ) ; :: thesis: f . n in the carrier of (PGraph X)

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 (PGraph X) ; :: thesis: verum

ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 )

proof

for n being Nat st 1 <= n & n <= len (PairF f) holds
A5:
(len f) -' 1 < ((len f) -' 1) + 1
by NAT_1:13;

let n be Nat; :: thesis: ( 1 <= n & n <= len (PairF f) implies ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 ) )

assume that

A6: 1 <= n and

A7: n <= len (PairF f) ; :: thesis: ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 )

A8: 1 < n + 1 by A6, NAT_1:13;

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

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

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

then A10: n < len f by A7, A9, A5, XXREAL_0:2;

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

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

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

n in dom f by A6, A10, FINSEQ_3:25;

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

then reconsider a = f . n, b = f . (n + 1) as Element of (PGraph X) by A11;

(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by A12, A11, FUNCT_3:def 5;

then A13: the Target of (PGraph X) . ((PairF f) . n) = b by A6, A10, Def2;

(pr1 (X,X)) . ((f . n),(f . (n + 1))) = f . n by A12, A11, FUNCT_3:def 4;

then the Source of (PGraph X) . ((PairF f) . n) = a by A6, A10, Def2;

then (PairF f) . n joins a,b by A13, GRAPH_1:def 12;

hence ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 ) ; :: thesis: verum

end;let n be Nat; :: thesis: ( 1 <= n & n <= len (PairF f) implies ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 ) )

assume that

A6: 1 <= n and

A7: n <= len (PairF f) ; :: thesis: ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 )

A8: 1 < n + 1 by A6, NAT_1:13;

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

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

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

then A10: n < len f by A7, A9, A5, XXREAL_0:2;

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

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

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

n in dom f by A6, A10, FINSEQ_3:25;

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

then reconsider a = f . n, b = f . (n + 1) as Element of (PGraph X) by A11;

(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by A12, A11, FUNCT_3:def 5;

then A13: the Target of (PGraph X) . ((PairF f) . n) = b by A6, A10, Def2;

(pr1 (X,X)) . ((f . n),(f . (n + 1))) = f . n by A12, A11, FUNCT_3:def 4;

then the Source of (PGraph X) . ((PairF f) . n) = a by A6, A10, Def2;

then (PairF f) . n joins a,b by A13, GRAPH_1:def 12;

hence ex x9, y9 being Element of (PGraph X) st

( x9 = f . n & y9 = f . (n + 1) & (PairF f) . n joins x9,y9 ) ; :: thesis: verum

(PairF f) . n in the carrier' of (PGraph X) by Th5;

hence PairF f is Chain of PGraph X by A2, A3, A4, GRAPH_1:def 14; :: thesis: verum

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 A14, 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;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 A14, 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

the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)

proof

hence
PairF f is oriented Chain of PGraph X
by A1, GRAPH_1:def 15; :: thesis: verum
A15:
(len f) -' 1 < ((len f) -' 1) + 1
by NAT_1:13;

let n be 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 that

A16: 1 <= n and

A17: n < len (PairF f) ; :: thesis: the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)

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

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

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

then A20: n < len f by A17, A18, A15, XXREAL_0:2;

then n in dom f by A16, FINSEQ_3:25;

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

n + 1 <= len (PairF f) by A17, NAT_1:13;

then A22: n + 1 < len f by A18, A19, A15, XXREAL_0:2;

then A23: (n + 1) + 1 <= len f by NAT_1:13;

A24: 1 < n + 1 by A16, NAT_1:13;

then 1 < (n + 1) + 1 by NAT_1:13;

then (n + 1) + 1 in dom f by A23, FINSEQ_3:25;

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

n + 1 <= len f by A20, NAT_1:13;

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

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

then reconsider b = f . (n + 1) as Element of (PGraph X) ;

(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by A21, A26, FUNCT_3:def 5;

then A27: the Target of (PGraph X) . ((PairF f) . n) = b by A16, A20, Def2;

n + 1 in dom f by A22, A24, FINSEQ_3:25;

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 A25, FUNCT_3:def 4;

hence the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n) by A22, A24, A27, Def2; :: thesis: verum

end;let n be 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 that

A16: 1 <= n and

A17: n < len (PairF f) ; :: thesis: the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n)

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

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

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

then A20: n < len f by A17, A18, A15, XXREAL_0:2;

then n in dom f by A16, FINSEQ_3:25;

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

n + 1 <= len (PairF f) by A17, NAT_1:13;

then A22: n + 1 < len f by A18, A19, A15, XXREAL_0:2;

then A23: (n + 1) + 1 <= len f by NAT_1:13;

A24: 1 < n + 1 by A16, NAT_1:13;

then 1 < (n + 1) + 1 by NAT_1:13;

then (n + 1) + 1 in dom f by A23, FINSEQ_3:25;

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

n + 1 <= len f by A20, NAT_1:13;

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

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

then reconsider b = f . (n + 1) as Element of (PGraph X) ;

(pr2 (X,X)) . ((f . n),(f . (n + 1))) = f . (n + 1) by A21, A26, FUNCT_3:def 5;

then A27: the Target of (PGraph X) . ((PairF f) . n) = b by A16, A20, Def2;

n + 1 in dom f by A22, A24, FINSEQ_3:25;

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 A25, FUNCT_3:def 4;

hence the Source of (PGraph X) . ((PairF f) . (n + 1)) = the Target of (PGraph X) . ((PairF f) . n) by A22, A24, A27, Def2; :: thesis: verum