let C be Category; :: thesis: for c, d being Object of C
for p1, p2, f being Morphism of 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, f being Morphism of 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, f be Morphism of 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, Def16;
then A3: 0 ,1 --> p1,p2 is Projections_family of c,{0 ,1} by Th48;
c is_a_product_wrt 0 ,1 --> p1,p2 by A1, Th59;
then d is_a_product_wrt (0 ,1 --> p1,p2) * f by A2, A3, Th56;
then d is_a_product_wrt 0 ,1 --> (p1 * f),(p2 * f) by Th18;
hence d is_a_product_wrt p1 * f,p2 * f by Th59; :: thesis: verum