let o, m be set ; :: thesis: c1Cat o,m is Cartesian
set 1PCat = c1Cat o,m;
thus the TerminalObj of (c1Cat o,m) is terminal by Th10; :: according to CAT_4:def 9 :: thesis: for a, b being Object of (c1Cat o,m) holds
( cod (the Proj1 of (c1Cat o,m) . a,b) = a & cod (the Proj2 of (c1Cat o,m) . a,b) = b & the CatProd of (c1Cat o,m) . a,b is_a_product_wrt the Proj1 of (c1Cat o,m) . a,b,the Proj2 of (c1Cat o,m) . a,b )
let a, b be Object of (c1Cat o,m); :: thesis: ( cod (the Proj1 of (c1Cat o,m) . a,b) = a & cod (the Proj2 of (c1Cat o,m) . a,b) = b & the CatProd of (c1Cat o,m) . a,b is_a_product_wrt the Proj1 of (c1Cat o,m) . a,b,the Proj2 of (c1Cat o,m) . a,b )
thus cod (the Proj1 of (c1Cat o,m) . a,b) = a by Th4; :: thesis: ( cod (the Proj2 of (c1Cat o,m) . a,b) = b & the CatProd of (c1Cat o,m) . a,b is_a_product_wrt the Proj1 of (c1Cat o,m) . a,b,the Proj2 of (c1Cat o,m) . a,b )
thus cod (the Proj2 of (c1Cat o,m) . a,b) = b by Th4; :: thesis: the CatProd of (c1Cat o,m) . a,b is_a_product_wrt the Proj1 of (c1Cat o,m) . a,b,the Proj2 of (c1Cat o,m) . a,b
thus the CatProd of (c1Cat o,m) . a,b is_a_product_wrt the Proj1 of (c1Cat o,m) . a,b,the Proj2 of (c1Cat o,m) . a,b by Th11; :: thesis: verum