let C be Cartesian_category; :: thesis: for a being Object of C holds
( Hom a,(a [x] ([1] C)) <> {} & Hom a,(([1] C) [x] a) <> {} )
let a be Object of C; :: thesis: ( Hom a,(a [x] ([1] C)) <> {} & Hom a,(([1] C) [x] a) <> {} )
( Hom a,([1] C) <> {} & Hom a,a <> {} ) by Th15, CAT_1:56;
hence ( Hom a,(a [x] ([1] C)) <> {} & Hom a,(([1] C) [x] a) <> {} ) by Th25; :: thesis: verum