defpred S₁[ Nat] means for p being non empty Graph-yielding FinSequence st len p = $1 & p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) holds
p . (len p) is edgeless ;
A1: S₁[1] ;
A2: for m being non zero Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non zero Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[m + 1]
let p be non empty Graph-yielding FinSequence; :: thesis: ( len p = m + 1 & p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) implies p . (len p) is edgeless )
assume that
A4: ( len p = m + 1 & p . 1 is edgeless ) and
A5: for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ; :: thesis: p . (len p) is edgeless
reconsider q = p | m as non empty Graph-yielding FinSequence ;
(m + 1) - 1 <= (len p) - 0 by A4, XREAL_1:10;
then A6: len q = m by FINSEQ_1:59;
A7: 1 <= m by INT_1:74;
then A8: q . 1 is edgeless by A4, FINSEQ_3:112;

now :: thesis: for n being Element of dom q st n <= (len q) - 1 holds
ex v being object st q . (n + 1) is addVertex of q . n,v

let n be Element of dom q; :: thesis: ( n <= (len q) - 1 implies ex v being object st q . (n + 1) is addVertex of q . n,v )
assume A9: n <= (len q) - 1 ; :: thesis: ex v being object st q . (n + 1) is addVertex of q . n,v
then n + 0 <= (m - 1) + 1 by A6, XREAL_1:7;
then A10: n <= (len p) - 1 by A4;
A11: ( 1 <= n & n <= len q ) by FINSEQ_3:25;
then ( 1 <= n & n + 0 <= m + 1 ) by A6, XREAL_1:7;
then reconsider k = n as Element of dom p by A4, FINSEQ_3:25;
consider v being object such that
A12: p . (k + 1) is addVertex of p . k,v by A5, A10;
take v = v; :: thesis: q . (n + 1) is addVertex of q . n,v
n + 1 <= ((len q) - 1) + 1 by A9, XREAL_1:6;
then ( p . (k + 1) = q . (n + 1) & p . k = q . k ) by A6, A11, FINSEQ_3:112;
hence q . (n + 1) is addVertex of q . n,v by A12; :: thesis: verum

end;

then A13: q . (len q) is edgeless by A3, A6, A8;
m + 0 <= ((len p) - 1) + 1 by A4, XREAL_1:6;
then reconsider k = m as Element of dom p by A7, FINSEQ_3:25;
consider v being object such that
A14: p . (k + 1) is addVertex of p . k,v by A5, A4;
p . k = q . (len q) by A6, FINSEQ_3:112;
hence p . (len p) is edgeless by A13, A4, A14; :: thesis: verum

end;

A15: for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A1, A2);
let p be non empty Graph-yielding FinSequence; :: thesis: ( p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) implies p . (len p) is edgeless )
assume A16: ( p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) ) ; :: thesis: p . (len p) is edgeless
thus p . (len p) is edgeless by A15, A16; :: thesis: verum