set TG = the Target of G;
set SG = the Source of G;
deffunc H1( Nat) -> set = the Source of G . (oc . $1);
consider z being FinSequence such that
A2:
( len z = len oc & ( for j being Nat st j in dom z holds
z . j = H1(j) ) )
from FINSEQ_1:sch 2();
set vs = z ^ <*( the Target of G . (oc . (len oc)))*>;
A3: len (z ^ <*( the Target of G . (oc . (len oc)))*>) =
(len oc) + (len <*( the Target of G . (oc . (len oc)))*>)
by A2, FINSEQ_1:22
.=
(len oc) + 1
by FINSEQ_1:39
;
A4:
Seg (len z) = dom z
by FINSEQ_1:def 3;
A5:
Seg (len oc) = dom oc
by FINSEQ_1:def 3;
0 + 1 = 1
;
then A6:
1 <= len oc
by A1, NAT_1:13;
rng (z ^ <*( the Target of G . (oc . (len oc)))*>) c= the carrier of G
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (z ^ <*( the Target of G . (oc . (len oc)))*>) or y in the carrier of G )
assume
y in rng (z ^ <*( the Target of G . (oc . (len oc)))*>)
;
y in the carrier of G
then consider x being
object such that A7:
x in dom (z ^ <*( the Target of G . (oc . (len oc)))*>)
and A8:
y = (z ^ <*( the Target of G . (oc . (len oc)))*>) . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A7;
A9:
1
<= x
by A7, FINSEQ_3:25;
A10:
x <= len (z ^ <*( the Target of G . (oc . (len oc)))*>)
by A7, FINSEQ_3:25;
per cases
( x <= len oc or x = (len oc) + 1 )
by A3, A10, NAT_1:8;
suppose A11:
x <= len oc
;
y in the carrier of GA12:
rng oc c= the
carrier' of
G
by FINSEQ_1:def 4;
A13:
x in dom oc
by A9, A11, FINSEQ_3:25;
then A14:
oc . x in rng oc
by FUNCT_1:def 3;
then reconsider e =
oc . x as
Element of the
carrier' of
G by A12;
A15:
the
Source of
G . e in rng the
Source of
G
by A14, A12, FUNCT_2:4;
A16:
rng the
Source of
G c= the
carrier of
G
by RELAT_1:def 19;
(z ^ <*( the Target of G . (oc . (len oc)))*>) . x =
z . x
by A2, A5, A4, A13, FINSEQ_1:def 7
.=
the
Source of
G . e
by A2, A5, A4, A13
;
hence
y in the
carrier of
G
by A8, A15, A16;
verum end; end;
end;
then reconsider vs = z ^ <*( the Target of G . (oc . (len oc)))*> as FinSequence of the carrier of G by FINSEQ_1:def 4;
take
vs
; ( vs is_vertex_seq_of oc & vs . 1 = the Source of G . (oc . 1) )
now ( len vs = (len oc) + 1 & ( for n being Nat st 1 <= n & n <= len oc holds
oc . n joins vs /. n,vs /. (n + 1) ) )thus
len vs = (len oc) + 1
by A3;
for n being Nat st 1 <= n & n <= len oc holds
oc . n joins vs /. n,vs /. (n + 1)let n be
Nat;
( 1 <= n & n <= len oc implies oc . n joins vs /. n,vs /. (n + 1) )assume that A21:
1
<= n
and A22:
n <= len oc
;
oc . n joins vs /. n,vs /. (n + 1)A23:
1
<= n + 1
by NAT_1:12;
n + 1
<= len vs
by A3, A22, XREAL_1:7;
then
n + 1
in dom vs
by A23, FINSEQ_3:25;
then reconsider vsn1 =
vs . (n + 1) as
Element of
G by FINSEQ_2:11;
A24:
vsn1 = vs /. (n + 1)
by A3, A22, A23, FINSEQ_4:15, XREAL_1:7;
A25:
vsn1 = the
Target of
G . (oc . n)
A28:
n <= len vs
by A3, A22, NAT_1:12;
then
n in dom vs
by A21, FINSEQ_3:25;
then reconsider vsn =
vs . n as
Element of
G by FINSEQ_2:11;
A29:
vsn = vs /. n
by A21, A28, FINSEQ_4:15;
A30:
n in dom oc
by A21, A22, FINSEQ_3:25;
then vsn =
z . n
by A2, A5, A4, FINSEQ_1:def 7
.=
the
Source of
G . (oc . n)
by A2, A5, A4, A30
;
hence
oc . n joins vs /. n,
vs /. (n + 1)
by A25, A29, A24;
verum end;
hence
vs is_vertex_seq_of oc
; vs . 1 = the Source of G . (oc . 1)
A31:
1 in dom z
by A2, A6, FINSEQ_3:25;
then
z . 1 = the Source of G . (oc . 1)
by A2;
hence
vs . 1 = the Source of G . (oc . 1)
by A31, FINSEQ_1:def 7; verum