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 Th3; :: according to CAT_3:def 15 :: 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 that
f in Hom (d,(cod p1)) and
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 Th5; :: 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 Th4; :: thesis: verum