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: c,d are_isomorphic
set I = {0 ,1};
set F = 0 ,1 --> p1,p2;
set F9 = 0 ,1 --> q1,q2;
A4: ( c is_a_product_wrt 0 ,1 --> p1,p2 & d is_a_product_wrt 0 ,1 --> q1,q2 ) by A1, A2, Th59;
( dom q1 = d & dom q2 = d ) by A2, Def16;
then A5: 0 ,1 --> q1,q2 is Projections_family of d,{0 ,1} by Th48;
( dom p1 = c & dom p2 = c ) by A1, Def16;
then A6: 0 ,1 --> p1,p2 is Projections_family of c,{0 ,1} by Th48;
cods (0 ,1 --> p1,p2) = 0 ,1 --> (cod q1),(cod q2) by A3, Th11
.= cods (0 ,1 --> q1,q2) by Th11 ;
hence c,d are_isomorphic by A6, A5, A4, Th53; :: thesis: verum