let C be Cartesian_category; :: thesis: for a, b, c being Object of C holds
( Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} & Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} )
let a, b, c be Object of C; :: thesis: ( Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} & Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} )
A1: Hom (a [x] b),a <> {} by Th21;
A2: Hom ((a [x] b) [x] c),(a [x] b) <> {} by Th21;
then A3: Hom ((a [x] b) [x] c),a <> {} by A1, CAT_1:52;
Hom (a [x] b),b <> {} by Th21;
then A4: Hom ((a [x] b) [x] c),b <> {} by A2, CAT_1:52;
Hom ((a [x] b) [x] c),c <> {} by Th21;
then Hom ((a [x] b) [x] c),(b [x] c) <> {} by A4, Th25;
hence Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} by A3, Th25; :: thesis: Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {}
A5: Hom (b [x] c),b <> {} by Th21;
A6: Hom (a [x] (b [x] c)),(b [x] c) <> {} by Th21;
then A7: Hom (a [x] (b [x] c)),b <> {} by A5, CAT_1:52;
Hom (b [x] c),c <> {} by Th21;
then A8: Hom (a [x] (b [x] c)),c <> {} by A6, CAT_1:52;
Hom (a [x] (b [x] c)),a <> {} by Th21;
then Hom (a [x] (b [x] c)),(a [x] b) <> {} by A7, Th25;
hence Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} by A8, Th25; :: thesis: verum