:: deftheorem defines is_exactly_partitable_wrt PUA2MSS1:def 9 :
for X being non empty set
for f being PartFunc of (X *),X
for P being a_partition of X holds
( f is_exactly_partitable_wrt P iff ( f is_partitable_wrt P & ( for p being FinSequence of P st product p meets dom f holds
product p c= dom f ) ) );