let C be Cartesian_category; 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; ( 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) [x] c),(a [x] b) <> {}
by Th21;
Hom (a [x] b),b <> {}
by Th21;
then A2:
Hom ((a [x] b) [x] c),b <> {}
by A1, CAT_1:52;
Hom (a [x] b),a <> {}
by Th21;
then A3:
Hom ((a [x] b) [x] c),a <> {}
by A1, CAT_1:52;
Hom ((a [x] b) [x] c),c <> {}
by Th21;
then
Hom ((a [x] b) [x] c),(b [x] c) <> {}
by A2, Th25;
hence
Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {}
by A3, Th25; Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {}
A4:
Hom (a [x] (b [x] c)),(b [x] c) <> {}
by Th21;
Hom (b [x] c),c <> {}
by Th21;
then A5:
Hom (a [x] (b [x] c)),c <> {}
by A4, CAT_1:52;
Hom (b [x] c),b <> {}
by Th21;
then A6:
Hom (a [x] (b [x] c)),b <> {}
by A4, CAT_1:52;
Hom (a [x] (b [x] c)),a <> {}
by Th21;
then
Hom (a [x] (b [x] c)),(a [x] b) <> {}
by A6, Th25;
hence
Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {}
by A5, Th25; verum