:: deftheorem defines disjoint_valued AOFA_A00:def 16 :
for J being non empty non void ManySortedSign
for T being MSAlgebra over J
for X being GeneratorSet of T
for A being ProgramAlgStr over J,T,X holds
( A is disjoint_valued iff ( the Sorts of T is disjoint_valued & the assignments of A is one-to-one ) );