let C be Category; 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; 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; 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; ( 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 )
; 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; verum