consider X being non empty finite set , P being a_partition of X;
take ProdMatroid P ; :: thesis: ( ProdMatroid P is finite & ProdMatroid P is strict )
thus ( ProdMatroid P is finite & ProdMatroid P is strict ) ; :: thesis: verum