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 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
.= (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 ;
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 ;
A10: x <= len (z ^ <*( the Target of G . (oc . (len oc)))*>) by ;
per cases ( x <= len oc or x = (len oc) + 1 ) by ;
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 ;
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 ;
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
.= 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 ;
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 ;
then y is Element of G by ;
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 ;
then n + 1 in dom vs by ;
then reconsider vsn1 = vs . (n + 1) as Element of G by FINSEQ_2:11;
A24: vsn1 = vs /. (n + 1) by ;
A25: vsn1 = the Target of G . (oc . n)
proof
per cases ( n < len oc or n = len oc ) by ;
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 ;
hence vsn1 = z . (n + 1) by
.= the Source of G . (oc . (n + 1)) by A2, A5, A4, A27
.= the Target of G . (oc . n) by ;
:: thesis: verum
end;
suppose n = len oc ; :: thesis: vsn1 = the Target of G . (oc . n)
hence vsn1 = the Target of G . (oc . n) by ; :: thesis: verum
end;
end;
end;
A28: n <= len vs by ;
then n in dom vs by ;
then reconsider vsn = vs . n as Element of G by FINSEQ_2:11;
A29: vsn = vs /. n by ;
A30: n in dom oc by ;
then vsn = z . n by
.= the Source of G . (oc . n) by A2, A5, A4, A30 ;
hence oc . n joins vs /. n,vs /. (n + 1) by ; :: 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 ;
then z . 1 = the Source of G . (oc . 1) by A2;
hence vs . 1 = the Source of G . (oc . 1) by ; :: thesis: verum