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,{0}) --> (p1,p2) by A1, Th54;
then d is_a_product_wrt ((0,{0}) --> (p1,p2)) * f by A2, Th51;
then d is_a_product_wrt (0,{0}) --> ((p1 (*) f),(p2 (*) f)) by Th14;
hence d is_a_product_wrt p1 (*) f,p2 (*) f by Th54; :: thesis: verum