for A being set 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