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