for P being mutually-disjoint set
for x being Subset of (ProdMatroid P) ex f being Function of x,P st
for a being object st a in x holds
a in f . a