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 A2, A5, XXREAL_0:2;

then A7: f /. k c= f /. j by A1, A3, A6, Th1;

defpred S_{1}[ Nat] means ( i + $1 <= j implies f /. j c= f /. (i + $1) );

_{1}[ 0 ]
by A4;

A14: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(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; :: thesis: verum

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 A2, A5, XXREAL_0:2;

then A7: f /. k c= f /. j by A1, A3, A6, Th1;

defpred S

A8: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A13:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A9: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A10: (i + k) + 1 = i + (k + 1) ;

thus S_{1}[k + 1]
:: thesis: verum

end;assume A9: S

A10: (i + k) + 1 = i + (k + 1) ;

thus S

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; :: thesis: verum

end;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; :: thesis: verum

A14: for k being Nat holds S

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; :: thesis: verum