:: deftheorem Def2 defines Cut HALLMAR1:def 2 :
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x being set
for b₅ being FinSequence of bool F holds
( b₅ = Cut (A,i,x) iff ( dom b₅ = dom A & ( for k being Element of NAT st k in dom b₅ holds
( ( i = k implies b₅ . k = (A . k) \ {x} ) & ( i <> k implies b₅ . k = A . k ) ) ) ) );