for C being Cartesian_category
for a, b being Object of C holds
( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a )