:: deftheorem Def74 defines AddFormulasTo FOMODEL4:def 74 :
for X being set
for S being Language
for D being RuleSet of S
for num being sequence of (AllFormulasOf S)
for b₅ being sequence of (bool (X \/ (AllFormulasOf S))) holds
( b₅ = (D,num) AddFormulasTo X iff ( b₅ . 0 = X & ( for m being Nat holds b₅ . (m + 1) = (D,(num . m)) AddFormulaTo (b₅ . m) ) ) );