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