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 Th13;
hence ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) by Th23; :: thesis: verum