:: deftheorem Def5 defines Complement PROB_3:def 5 :
for X being set
for F1, b₃ being FinSequence of bool X holds
( b₃ = Complement F1 iff ( len b₃ = len F1 & ( for n being Nat st n in dom b₃ holds
b₃ . n = (F1 . n) ` ) ) );