union P is finite ;
hence the carrier of (ProdMatroid P) is finite by Def7; :: according to STRUCT_0:def 11 :: thesis: verum