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 Th49; :: according to CAT_3:def 19 :: 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
( f in Hom (dom i1),d & 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 Th52; :: 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 Th51; :: thesis: verum