let C be Category; :: thesis: for d, c 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 d, c 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
( dom p1 = c & dom p2 = c ) by A1, Def15;
then A3: (0,1) --> (p1,p2) is Projections_family of c,{0,1} by Th44;
c is_a_product_wrt (0,1) --> (p1,p2) by A1, Th54;
then d is_a_product_wrt ((0,1) --> (p1,p2)) * f by A2, A3, Th51;
then d is_a_product_wrt (0,1) --> ((p1 (*) f),(p2 (*) f)) by Th14;
hence d is_a_product_wrt p1 (*) f,p2 (*) f by Th54; :: thesis: verum