let V be set ; :: thesis:
let G be Graph; :: thesis:
let pe be FinSequence of the carrier' of G; :: thesis:
defpred S₁[ Nat] means ( $1 in dom pe & not vertices (pe /. $1) c= V );
assume not vertices pe c= V ; :: thesis:
then A1: ex i being Nat st S₁[i] by Th17;
consider k being Nat such that
A2: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A1);
k <= len pe by A2, FINSEQ_3:25;
then consider j being Nat such that
A3: len pe = k + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
1 <= k by A2, FINSEQ_3:25;
then consider i being Nat such that
A4: k = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
len pe = i + (1 + j) by A4, A3;
then consider q, r being FinSequence such that
A5: len q = i and
len r = 1 + j and
A6: pe = q ^ r by FINSEQ_2:22;
reconsider q = q, r = r as FinSequence of the carrier' of G by A6, FINSEQ_1:36;
take i ; :: thesis:
take q ; :: thesis:
take r ; :: thesis:
thus ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V ) by A2, A4, FINSEQ_3:25; :: thesis:
thus ( len q = i & pe = q ^ r ) by A5, A6; :: thesis:

end;