let X be non empty set ; for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is V30()
let s be sequence of X; ( ( for i being Nat holds s . i = s . (i + 1) ) implies s is V30() )
assume A1:
for i being Nat holds s . i = s . (i + 1)
; s is V30()
now for i, j being Nat holds s . i = s . jlet i,
j be
Nat;
s . i = s . jA2:
now for i, j being Nat st i <= j holds
s . i = s . jlet i,
j be
Nat;
( i <= j implies s . i = s . j )assume A3:
i <= j
;
s . i = s . jdefpred S1[
Nat]
means (
i <= $1 implies
s . i = s . $1 );
A4:
for
j being
Nat st
S1[
j] holds
S1[
j + 1]
A6:
S1[
0 ]
by NAT_1:3;
for
j being
Nat holds
S1[
j]
from NAT_1:sch 2(A6, A4);
hence
s . i = s . j
by A3;
verum end;
(
i <= j or
j <= i )
;
hence
s . i = s . j
by A2;
verum end;
hence
s is V30()
; verum