let X be non empty set ; for f being FinSequence of X holds PairF f is oriented Chain of PGraph X
let f be FinSequence of X; PairF f is oriented Chain of PGraph X
A1:
now ( ( 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
;
PairF f is Chain of PGraph Xthen
((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)
A4:
for
n being
Nat st 1
<= n &
n <= len (PairF f) holds
ex
x9,
y9 being
Element of
(PGraph X) st
(
x9 = f . n &
y9 = f . (n + 1) &
(PairF f) . n joins x9,
y9 )
proof
A5:
(len f) -' 1
< ((len f) -' 1) + 1
by NAT_1:13;
let n be
Nat;
( 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)
;
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 )
;
verum
end;
for
n being
Nat st 1
<= n &
n <= len (PairF f) holds
(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;
verum end;
for n being 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
A15:
(len f) -' 1
< ((len f) -' 1) + 1
by NAT_1:13;
let n be
Nat;
( 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)
;
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;
verum
end;
hence
PairF f is oriented Chain of PGraph X
by A1, GRAPH_1:def 15; verum