let o, m be set ; :: thesis: for c being Object of (c1Cat* (o,m))
for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2
let c be Object of (c1Cat* (o,m)); :: thesis: for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2
let i1, i2 be Morphism of (c1Cat* (o,m)); :: thesis: c is_a_coproduct_wrt i1,i2
thus ( cod i1 = c & cod i2 = c ) by Th45; :: according to CAT_3:def 18 :: 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 ((dom i1),b1) or not b3 in Hom ((dom i2),b1) or ex b4 being Element of the carrier' of (c1Cat* (o,m)) st
( b4 in Hom (c,b1) & ( for b5 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b5 in Hom (c,b1) or ( ( not b5 (*) i1 = b2 or not b5 (*) i2 = b3 or b4 = b5 ) & ( not b4 = b5 or ( b5 (*) i1 = b2 & b5 (*) i2 = 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 ((dom i1),d) or not b2 in Hom ((dom i2),d) or ex b3 being Element of the carrier' of (c1Cat* (o,m)) st
( b3 in Hom (c,d) & ( for b4 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b4 in Hom (c,d) or ( ( not b4 (*) i1 = b1 or not b4 (*) i2 = b2 or b3 = b4 ) & ( not b3 = b4 or ( b4 (*) i1 = b1 & b4 (*) i2 = b2 ) ) ) ) ) ) )
let f, g be Morphism of (c1Cat* (o,m)); :: thesis: ( not f in Hom ((dom i1),d) or not g in Hom ((dom i2),d) or ex b1 being Element of the carrier' of (c1Cat* (o,m)) st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) ) )
assume that
f in Hom ((dom i1),d) and
g in Hom ((dom i2),d) ; :: thesis: ex b1 being Element of the carrier' of (c1Cat* (o,m)) st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) )
take h = i1; :: thesis: ( h in Hom (c,d) & ( for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) ) )
thus h in Hom (c,d) by Th47; :: thesis: for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) )
thus for b1 being Element of the carrier' of (c1Cat* (o,m)) holds
( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) by Th46; :: thesis: verum