let o, m be set ; :: thesis: c1Cat* (o,m) is Cocartesian
set 1PCat = c1Cat* (o,m);
thus the Initial of (c1Cat* (o,m)) is initial by Th55; :: according to CAT_4:def 26 :: thesis: for a, b being Object of (c1Cat* (o,m)) holds
( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
let a, b be Object of (c1Cat* (o,m)); :: thesis: ( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
thus dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a by Th49; :: thesis: ( dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) )
thus dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b by Th49; :: thesis: the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b)
thus the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) by Th56; :: thesis: verum