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 Th19;
Hom ((a [x] b),b) <> {}
by Th19;
then A2:
Hom (((a [x] b) [x] c),b) <> {}
by A1, CAT_1:24;
Hom ((a [x] b),a) <> {}
by Th19;
then A3:
Hom (((a [x] b) [x] c),a) <> {}
by A1, CAT_1:24;
Hom (((a [x] b) [x] c),c) <> {}
by Th19;
then
Hom (((a [x] b) [x] c),(b [x] c)) <> {}
by A2, Th23;
hence
Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {}
by A3, Th23; Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {}
A4:
Hom ((a [x] (b [x] c)),(b [x] c)) <> {}
by Th19;
Hom ((b [x] c),c) <> {}
by Th19;
then A5:
Hom ((a [x] (b [x] c)),c) <> {}
by A4, CAT_1:24;
Hom ((b [x] c),b) <> {}
by Th19;
then A6:
Hom ((a [x] (b [x] c)),b) <> {}
by A4, CAT_1:24;
Hom ((a [x] (b [x] c)),a) <> {}
by Th19;
then
Hom ((a [x] (b [x] c)),(a [x] b)) <> {}
by A6, Th23;
hence
Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {}
by A5, Th23; verum