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 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Nat st i <= k & k <= j holds
f /. j = f /. k

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 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Nat st i <= k & k <= j holds
f /. j = f /. k )

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 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Nat st i <= k & k <= j holds
f /. j = f /. k

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

assume that
A2: 1 <= i and
A3: j <= len f and
A4: f /. j c= f /. i ; :: thesis: for k being Nat st i <= k & k <= j holds
f /. j = f /. k

let k be Nat; :: thesis: ( i <= k & k <= j implies f /. j = f /. k )
assume that
A5: i <= k and
A6: k <= j ; :: thesis: f /. j = f /. k
1 <= k by ;
then A7: f /. k c= f /. j by A1, A3, A6, Th1;
defpred S1[ Nat] means ( i + \$1 <= j implies f /. j c= f /. (i + \$1) );
A8: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
A10: (i + k) + 1 = i + (k + 1) ;
thus S1[k + 1] :: thesis: verum
proof
i + k >= i by NAT_1:11;
then A11: i + k >= 1 by ;
assume A12: i + (k + 1) <= j ; :: thesis: f /. j 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 ;
hence f /. j c= f /. (i + (k + 1)) by ; :: thesis: verum
end;
end;
A13: S1[ 0 ] by A4;
A14: for k being Nat holds S1[k] from NAT_1:sch 2(A13, A8);
consider m being Nat such that
A15: k = i + m by ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
k = i + m by A15;
then f /. j c= f /. k by ;
hence f /. j = f /. k by A7; :: thesis: verum