theorem Th1: :: FIN_TOPO:1

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 i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j