let C be Category; :: thesis: for c, d being Object of C
for p1, p2 being Morphism of C
for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 (*) f,p2 (*) f

let c, d be Object of C; :: thesis: for p1, p2 being Morphism of C
for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 (*) f,p2 (*) f

let p1, p2 be Morphism of C; :: thesis: for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 (*) f,p2 (*) f

let f be Morphism of d,c; :: thesis: ( c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible implies d is_a_product_wrt p1 (*) f,p2 (*) f )
assume that
A1: c is_a_product_wrt p1,p2 and
A2: ( dom f = d & cod f = c & f is invertible ) ; :: thesis: d is_a_product_wrt p1 (*) f,p2 (*) f
c is_a_product_wrt (0,) --> (p1,p2) by ;
then d is_a_product_wrt ((0,) --> (p1,p2)) * f by ;
then d is_a_product_wrt (0,) --> ((p1 (*) f),(p2 (*) f)) by Th14;
hence d is_a_product_wrt p1 (*) f,p2 (*) f by Th54; :: thesis: verum