consider B being Object of C, P being MorphismsFamily of A,B such that
A1: ( P is feasible & P is coprojection-morphisms ) by Def7;
take B ; :: thesis: B is A -CatCoproduct-like
take P ; :: according to ALTCAT_6:def 8 :: thesis: ( P is feasible & P is coprojection-morphisms )
thus ( P is feasible & P is coprojection-morphisms ) by A1; :: thesis: verum