let o, m be set ; :: thesis: for c being Object of (c1Cat o,m)
for p1, p2 being Morphism of (c1Cat o,m) holds c is_a_product_wrt p1,p2
let c be Object of (c1Cat o,m); :: thesis: for p1, p2 being Morphism of (c1Cat o,m) holds c is_a_product_wrt p1,p2
let p1, p2 be Morphism of (c1Cat o,m); :: thesis: c is_a_product_wrt p1,p2
thus
( dom p1 = c & dom p2 = c )
by Th4; :: according to CAT_3:def 16 :: thesis: for b1 being Element of the carrier of (c1Cat o,m)
for b2, b3 being Element of the carrier' of (c1Cat o,m) holds
( not b2 in Hom b1,(cod p1) or not b3 in Hom b1,(cod p2) or ex b4 being Element of the carrier' of (c1Cat o,m) st
( b4 in Hom b1,c & ( for b5 being Element of the carrier' of (c1Cat o,m) holds
( not b5 in Hom b1,c or ( ( not p1 * b5 = b2 or not p2 * b5 = b3 or b4 = b5 ) & ( not b4 = b5 or ( p1 * b5 = b2 & p2 * b5 = b3 ) ) ) ) ) ) )
let d be Object of (c1Cat o,m); :: thesis: for b1, b2 being Element of the carrier' of (c1Cat o,m) holds
( not b1 in Hom d,(cod p1) or not b2 in Hom d,(cod p2) or ex b3 being Element of the carrier' of (c1Cat o,m) st
( b3 in Hom d,c & ( for b4 being Element of the carrier' of (c1Cat o,m) holds
( not b4 in Hom d,c or ( ( not p1 * b4 = b1 or not p2 * b4 = b2 or b3 = b4 ) & ( not b3 = b4 or ( p1 * b4 = b1 & p2 * b4 = b2 ) ) ) ) ) ) )
let f, g be Morphism of (c1Cat o,m); :: thesis: ( not f in Hom d,(cod p1) or not g in Hom d,(cod p2) or ex b1 being Element of the carrier' of (c1Cat o,m) st
( b1 in Hom d,c & ( for b2 being Element of the carrier' of (c1Cat o,m) holds
( not b2 in Hom d,c or ( ( not p1 * b2 = f or not p2 * b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 * b2 = f & p2 * b2 = g ) ) ) ) ) ) )
assume
( f in Hom d,(cod p1) & g in Hom d,(cod p2) )
; :: thesis: ex b1 being Element of the carrier' of (c1Cat o,m) st
( b1 in Hom d,c & ( for b2 being Element of the carrier' of (c1Cat o,m) holds
( not b2 in Hom d,c or ( ( not p1 * b2 = f or not p2 * b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 * b2 = f & p2 * b2 = g ) ) ) ) ) )
take h = p1; :: thesis: ( h in Hom d,c & ( for b1 being Element of the carrier' of (c1Cat o,m) holds
( not b1 in Hom d,c or ( ( not p1 * b1 = f or not p2 * b1 = g or h = b1 ) & ( not h = b1 or ( p1 * b1 = f & p2 * b1 = g ) ) ) ) ) )
thus
h in Hom d,c
by Th7; :: thesis: for b1 being Element of the carrier' of (c1Cat o,m) holds
( not b1 in Hom d,c or ( ( not p1 * b1 = f or not p2 * b1 = g or h = b1 ) & ( not h = b1 or ( p1 * b1 = f & p2 * b1 = g ) ) ) )
thus
for b1 being Element of the carrier' of (c1Cat o,m) holds
( not b1 in Hom d,c or ( ( not p1 * b1 = f or not p2 * b1 = g or h = b1 ) & ( not h = b1 or ( p1 * b1 = f & p2 * b1 = g ) ) ) )
by Th6; :: thesis: verum