let X be non empty set ; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: s is V30()
now :: thesis: for i, j being Nat holds s . i = s . j
let i, j be Nat; :: thesis: s . i = s . j
A2: now :: thesis: for i, j being Nat st i <= j holds
s . i = s . j
let i, j be Nat; :: thesis: ( i <= j implies s . i = s . j )
assume A3: i <= j ; :: thesis: s . i = s . j
defpred S1[ Nat] means ( i <= $1 implies s . i = s . $1 );
A4: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A5: S1[j] ; :: thesis: S1[j + 1]
assume i <= j + 1 ; :: thesis: s . i = s . (j + 1)
then ( i < j + 1 or i = j + 1 ) by XXREAL_0:1;
hence s . i = s . (j + 1) by A1, A5, NAT_1:13; :: thesis: verum
end;
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; :: thesis: verum
end;
( i <= j or j <= i ) ;
hence s . i = s . j by A2; :: thesis: verum
end;
hence s is V30() ; :: thesis: verum