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 27 :: 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