consider B being Object of C, P being MorphismsFamily of B,A such that
A1: ( P is feasible & P is projection-morphisms ) by Def8;
take B ; :: thesis: B is A -CatProduct-like
take P ; :: according to ALTCAT_5:def 9 :: thesis: ( P is feasible & P is projection-morphisms )
thus ( P is feasible & P is projection-morphisms ) by A1; :: thesis: verum