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₁[ Nat] means ( i + $1 <= j implies f /. i c= f /. (i + $1) );

A6: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A7: (i + k) + 1 = i + (k + 1) ;
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

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;

end;

A11: S₁[ 0 ] ;
A12: for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A6);
thus f /. i c= f /. j by A12, A5; :: thesis: verum