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 A2, NAT_1:10;

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

_{1}[ 0 ]
;

A12: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A11, A6);

thus f /. i c= f /. j by A12, A5; :: thesis: verum

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 A2, NAT_1:10;

defpred S

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

S_{1}[k + 1]

A11:
SS

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

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

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

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

end;A7: (i + k) + 1 = i + (k + 1) ;

assume A8: S

thus S

proof

i + k >= i
by NAT_1:11;

then A9: i + k >= 1 by A3, XXREAL_0:2;

assume A10: i + (k + 1) <= j ; :: thesis: f /. i c= f /. (i + (k + 1))

then i + k < j by A7, NAT_1:13;

then i + k < len f by A4, XXREAL_0:2;

then f /. (i + k) c= f /. (i + (k + 1)) by A1, A7, A9;

hence f /. i c= f /. (i + (k + 1)) by A7, A8, A10, NAT_1:13; :: thesis: verum

end;then A9: i + k >= 1 by A3, XXREAL_0:2;

assume A10: i + (k + 1) <= j ; :: thesis: f /. i c= f /. (i + (k + 1))

then i + k < j by A7, NAT_1:13;

then i + k < len f by A4, XXREAL_0:2;

then f /. (i + k) c= f /. (i + (k + 1)) by A1, A7, A9;

hence f /. i c= f /. (i + (k + 1)) by A7, A8, A10, NAT_1:13; :: thesis: verum

A12: for k being Nat holds S

thus f /. i c= f /. j by A12, A5; :: thesis: verum