let C be Category; :: thesis: for c, d being Object of C
for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds
c,d are_isomorphic

let c, d be Object of C; :: thesis: for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds
c,d are_isomorphic

let p1, p2, q1, q2 be Morphism of C; :: thesis: ( c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 implies c,d are_isomorphic )
assume that
A1: c is_a_product_wrt p1,p2 and
A2: d is_a_product_wrt q1,q2 and
A3: ( cod p1 = cod q1 & cod p2 = cod q2 ) ; :: thesis:
set I = ;
set F = (0,) --> (p1,p2);
set F9 = (0,) --> (q1,q2);
A4: ( c is_a_product_wrt (0,) --> (p1,p2) & d is_a_product_wrt (0,) --> (q1,q2) ) by A1, A2, Th54;
cods ((0,) --> (p1,p2)) = (0,) --> ((cod q1),(cod q2)) by
.= cods ((0,) --> (q1,q2)) by Th7 ;
hence c,d are_isomorphic by ; :: thesis: verum