set TG = the Target of G;
set SG = the Source of G;
deffunc H₁( 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 = H₁(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 ; :: according to TARSKI:def 3 :: thesis: ( 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)))*>) ; :: thesis: 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 ; :: thesis: y in the carrier of G

A12: 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; :: thesis: verum

end;

suppose A17: x = (len oc) + 1 ; :: thesis: y in the carrier of G

len oc in dom oc by A6, FINSEQ_3:25;
then A18: oc . (len oc) in rng oc by FUNCT_1:def 3;
A19: rng oc c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = oc . (len oc) as Element of the carrier' of G by A18;
A20: rng the Target of G c= the carrier of G by RELAT_1:def 19;
the Target of G . e in rng the Target of G by A18, A19, FUNCT_2:4;
then y is Element of G by A2, A8, A17, A20, FINSEQ_1:42;
hence y in the carrier of G ; :: thesis: 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 ; :: thesis: ( vs is_vertex_seq_of oc & vs . 1 = the Source of G . (oc . 1) )

now :: thesis: ( 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; :: thesis: for n being Nat st 1 <= n & n <= len oc holds
oc . n joins vs /. n,vs /. (n + 1)
let n be Nat; :: thesis: ( 1 <= n & n <= len oc implies oc . n joins vs /. n,vs /. (n + 1) )
assume that
A21: 1 <= n and
A22: n <= len oc ; :: thesis: 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)

proof

per cases ( n < len oc or n = len oc ) by A22, XXREAL_0:1;

suppose A26: n < len oc ; :: thesis: vsn1 = the Target of G . (oc . n)

then n + 1 <= len oc by NAT_1:13;
then A27: n + 1 in dom oc by A23, FINSEQ_3:25;
hence vsn1 = z . (n + 1) by A2, A5, A4, FINSEQ_1:def 7
.= the Source of G . (oc . (n + 1)) by A2, A5, A4, A27
.= the Target of G . (oc . n) by A21, A26, GRAPH_1:def 15 ;
:: thesis: verum

end;

suppose n = len oc ; :: thesis: vsn1 = the Target of G . (oc . n)

hence vsn1 = the Target of G . (oc . n) by A2, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

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; :: thesis: verum

end;

hence vs is_vertex_seq_of oc ; :: thesis: 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; :: thesis: verum