let A be set ; :: thesis: for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let f be FinSequence of bool A; :: thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k )
assume A1: for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; :: thesis: for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let i, j be Element of NAT ; :: thesis: ( 1 <= i & j <= len f & f /. j c= f /. i implies for k being Element of 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 Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let k be Element of 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 A2, A5, XXREAL_0:2;
then A7: f /. k c= f /. j by A1, A3, A6, Th1;
defpred S₁[ Element of NAT ] means ( i + $1 <= j implies f /. j c= f /. (i + $1) );

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
A10: (i + k) + 1 = i + (k + 1) ;
thus S₁[k + 1] :: thesis: verum

proof

i + k >= i by NAT_1:11;
then A11: i + k >= 1 by A2, XXREAL_0:2;
assume A12: i + (k + 1) <= j ; :: thesis: f /. j c= f /. (i + (k + 1))
then i + k < j by A10, NAT_1:13;
then i + k < len f by A3, XXREAL_0:2;
then f /. (i + k) c= f /. ((i + k) + 1) by A1, A11;
hence f /. j c= f /. (i + (k + 1)) by A9, A12, NAT_1:13, XBOOLE_1:1; :: thesis: verum

end;

end;

A13: S₁[ 0 ] by A4;
A14: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A13, A8);
consider m being Nat such that
A15: k = i + m by A5, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
k = i + m by A15;
then f /. j c= f /. k by A14, A6;
hence f /. j = f /. k by A7, XBOOLE_0:def 10; :: thesis: verum