let A be set ; :: thesis: for f being FinSequence of bool A st ( for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Nat st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j

let f be FinSequence of bool A; :: thesis: ( ( for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Nat st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j )

assume A1: for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; :: thesis: for i, j being Nat st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j

let i, j be Nat; :: thesis: ( i <= j & 1 <= i & j <= len f implies f /. i c= f /. j )
assume that
A2: i <= j and
A3: 1 <= i and
A4: j <= len f ; :: thesis: f /. i c= f /. j
consider k being Nat such that
A5: i + k = j by ;
defpred S1[ Nat] means ( i + \$1 <= j implies f /. i c= f /. (i + \$1) );
A6: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A7: (i + k) + 1 = i + (k + 1) ;
assume A8: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
i + k >= i by NAT_1:11;
then A9: i + k >= 1 by ;
assume A10: i + (k + 1) <= j ; :: thesis: f /. i c= f /. (i + (k + 1))
then i + k < j by ;
then i + k < len f by ;
then f /. (i + k) c= f /. (i + (k + 1)) by A1, A7, A9;
hence f /. i c= f /. (i + (k + 1)) by ; :: thesis: verum
end;
end;
A11: S1[ 0 ] ;
A12: for k being Nat holds S1[k] from NAT_1:sch 2(A11, A6);
thus f /. i c= f /. j by ; :: thesis: verum