:: deftheorem Def64 defines Tau MODELC_1:def 64 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T being Subset of S
for b₅ being Assign of (BASSModel (R,BASSIGN)) holds
( b₅ = Tau (T,R,BASSIGN) iff for s being set st s in S holds
(Fid (b₅,S)) . s = (chi (T,S)) . s );