set TG = the Target of G;

set SG = the Source of G;

deffunc H_{1}( 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_{1}(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

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

set SG = the Source of G;

deffunc H

consider z being FinSequence such that

A2: ( len z = len oc & ( for j being Nat st j in dom z holds

z . j = H

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

then reconsider vs = z ^ <*( the Target of G . (oc . (len oc)))*> as FinSequence of the carrier of G by FINSEQ_1:def 4;
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;

end;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;

end;

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;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

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;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

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) ) )

hence
vs is_vertex_seq_of oc
; :: thesis: vs . 1 = the Source of G . (oc . 1)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)

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;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
end;

A28:
n <= len vs
by A3, A22, NAT_1:12;per cases
( n < len oc or n = len oc )
by A22, XXREAL_0:1;

end;

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;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

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

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