:: deftheorem defines InputValues MSAFREE2:def 5 :
for S being non empty ManySortedSign
for MSA being non-empty MSAlgebra over S
for b₃ being ManySortedSet of InputVertices S holds
( b₃ is InputValues of MSA iff for v being Vertex of S st v in InputVertices S holds
b₃ . v in the Sorts of MSA . v );