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 i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
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 i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j )
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 i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
let i, j be Element of NAT ; :: thesis: ( i <= j & 1 <= i & j <= len f implies f /. i c= f /. j )
assume A2: ( i <= j & 1 <= i & j <= len f ) ; :: thesis: f /. i c= f /. j
defpred S₁[ Element of NAT ] means ( i + $1 <= j implies f /. i c= f /. (i + $1) );
A3: S₁[ 0 ] ;

A4: now

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

proof

assume A7: i + (k + 1) <= j ; :: thesis: f /. i c= f /. (i + (k + 1))
then A8: i + k < j by A5, NAT_1:13;
i + k >= i by NAT_1:11;
then ( i + k >= 1 & i + k < len f ) by A2, A8, XXREAL_0:2;
then f /. (i + k) c= f /. (i + (k + 1)) by A1, A5;
hence f /. i c= f /. (i + (k + 1)) by A5, A6, A7, NAT_1:13, XBOOLE_1:1; :: thesis: verum

end;

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
consider k being Nat such that
A10: i + k = j by A2, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence f /. i c= f /. j by A9, A10; :: thesis: verum