let X be non empty set ; for f being FinSequence of X
for f1 being FinSequence of the carrier of (PGraph X) st len f >= 1 & f = f1 holds
f1 is_oriented_vertex_seq_of PairF f
let f be FinSequence of X; for f1 being FinSequence of the carrier of (PGraph X) st len f >= 1 & f = f1 holds
f1 is_oriented_vertex_seq_of PairF f
let f1 be FinSequence of the carrier of (PGraph X); ( len f >= 1 & f = f1 implies f1 is_oriented_vertex_seq_of PairF f )
assume that
A1:
len f >= 1
and
A2:
f = f1
; f1 is_oriented_vertex_seq_of PairF f
A3:
for n being Nat st 1 <= n & n <= len (PairF f) holds
(PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1)
proof
A4:
(len f) -' 1
< ((len f) -' 1) + 1
by NAT_1:13;
let n be
Nat;
( 1 <= n & n <= len (PairF f) implies (PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1) )
assume that A5:
1
<= n
and A6:
n <= len (PairF f)
;
(PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1)
A7:
1
< n + 1
by A5, NAT_1:13;
A8:
len (PairF f) = (len f) -' 1
by Def2;
then
1
<= (len f) -' 1
by A5, A6, XXREAL_0:2;
then
(len f) -' 1
= (len f) - 1
by NAT_D:39;
then A9:
n < len f
by A6, A8, A4, XXREAL_0:2;
then
n + 1
<= len f
by NAT_1:13;
then A10:
n + 1
in dom f
by A7, FINSEQ_3:25;
then A11:
f . (n + 1) in rng f
by FUNCT_1:def 3;
A12:
n in dom f
by A5, A9, FINSEQ_3:25;
then A13:
f . n in rng f
by FUNCT_1:def 3;
then A14:
(pr1 (X,X)) . (
(f . n),
(f . (n + 1)))
= f . n
by A11, FUNCT_3:def 4;
A15:
(pr2 (X,X)) . (
(f . n),
(f . (n + 1)))
= f . (n + 1)
by A13, A11, FUNCT_3:def 5;
f1 /. (n + 1) = f1 . (n + 1)
by A2, A10, PARTFUN1:def 6;
then A16:
the
Target of
(PGraph X) . ((PairF f) . n) = f1 /. (n + 1)
by A2, A5, A9, A15, Def2;
f1 /. n = f1 . n
by A2, A12, PARTFUN1:def 6;
then
the
Source of
(PGraph X) . ((PairF f) . n) = f1 /. n
by A2, A5, A9, A14, Def2;
hence
(PairF f) . n orientedly_joins f1 /. n,
f1 /. (n + 1)
by A16, GRAPH_4:def 1;
verum
end;
A17:
for n being Nat st 1 <= n & n <= len (PairF f) holds
(PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1)
by A3;
(len f) -' 1 = (len f) - 1
by A1, XREAL_1:233;
then
((len f) - 1) + 1 = (len (PairF f)) + 1
by Def2;
hence
f1 is_oriented_vertex_seq_of PairF f
by A2, A17, GRAPH_4:def 5; verum