:: deftheorem Def71 defines AddWitnessesTo FOMODEL4:def 71 :
for X being functional set
for S being Language
for D being RuleSet of S
for num being sequence of (ExFormulasOf S)
for b₅ being sequence of (bool (X \/ (AllFormulasOf S))) holds
( b₅ = (D,num) AddWitnessesTo X iff ( b₅ . 0 = X & ( for mm being Element of NAT holds b₅ . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b₅ . mm) ) ) );