let X be non empty set ; :: thesis: 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; :: thesis: 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); :: thesis: ( len f >= 1 & f = f1 implies f1 is_oriented_vertex_seq_of PairF f )
assume A1:
( len f >= 1 & f = f1 )
; :: thesis: f1 is_oriented_vertex_seq_of PairF f
then
(len f) -' 1 = (len f) - 1
by XREAL_1:235;
then A2:
((len f) - 1) + 1 = (len (PairF f)) + 1
by Def2;
for n being Element of NAT st 1 <= n & n <= len (PairF f) holds
(PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1)
proof
let n be
Element of
NAT ;
:: thesis: ( 1 <= n & n <= len (PairF f) implies (PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1) )
assume A3:
( 1
<= n &
n <= len (PairF f) )
;
:: thesis: (PairF f) . n orientedly_joins f1 /. n,f1 /. (n + 1)
A4:
len (PairF f) = (len f) -' 1
by Def2;
then
1
<= (len f) -' 1
by A3, XXREAL_0:2;
then A5:
(len f) -' 1
= (len f) - 1
by NAT_D:39;
(len f) -' 1
< ((len f) -' 1) + 1
by NAT_1:13;
then A6:
n < len f
by A3, A4, A5, XXREAL_0:2;
then A7:
n in dom f
by A3, FINSEQ_3:27;
then A8:
f . n in rng f
by FUNCT_1:def 5;
A9:
1
< n + 1
by A3, NAT_1:13;
n + 1
<= len f
by A6, NAT_1:13;
then A10:
n + 1
in dom f
by A9, FINSEQ_3:27;
then A11:
f . (n + 1) in rng f
by FUNCT_1:def 5;
A12:
f1 /. n = f1 . n
by A1, A7, PARTFUN1:def 8;
A13:
f1 /. (n + 1) = f1 . (n + 1)
by A1, A10, PARTFUN1:def 8;
A14:
(pr1 X,X) . (f . n),
(f . (n + 1)) = f . n
by A8, A11, FUNCT_3:def 5;
(pr2 X,X) . (f . n),
(f . (n + 1)) = f . (n + 1)
by A8, A11, FUNCT_3:def 6;
then
( the
Source of
(PGraph X) . ((PairF f) . n) = f1 /. n & the
Target of
(PGraph X) . ((PairF f) . n) = f1 /. (n + 1) )
by A1, A3, A6, A12, A13, A14, Def2;
hence
(PairF f) . n orientedly_joins f1 /. n,
f1 /. (n + 1)
by GRAPH_4:def 1;
:: thesis: verum
end;
hence
f1 is_oriented_vertex_seq_of PairF f
by A1, A2, GRAPH_4:def 5; :: thesis: verum