for P being mutually-disjoint set
for x being Subset of (ProdMatroid P)
for f being Function of x,P st ( for a being object st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )