let C be Cartesian_category; :: thesis: for a, b, c being Object of C holds
( (Alpha a,b,c) * (Alpha' a,b,c) = id (a [x] (b [x] c)) & (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c) )
let a, b, c be Object of C; :: thesis: ( (Alpha a,b,c) * (Alpha' a,b,c) = id (a [x] (b [x] c)) & (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c) )
set k = <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>;
set l = <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>;
set f = <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:>;
set g = <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):>;
A1: Hom ((a [x] b) [x] c),(a [x] b) <> {} by Th21;
A2: Hom (a [x] b),b <> {} by Th21;
then A3: Hom ((a [x] b) [x] c),b <> {} by A1, CAT_1:52;
A4: Hom ((a [x] b) [x] c),c <> {} by Th21;
then A5: Hom ((a [x] b) [x] c),(b [x] c) <> {} by A3, Th25;
A6: Hom (a [x] b),a <> {} by Th21;
then A7: Hom ((a [x] b) [x] c),a <> {} by A1, CAT_1:52;
A8: Hom (a [x] (b [x] c)),(b [x] c) <> {} by Th21;
A9: Hom (b [x] c),c <> {} by Th21;
then A10: Hom (a [x] (b [x] c)),c <> {} by A8, CAT_1:52;
A11: Hom (b [x] c),b <> {} by Th21;
then A12: Hom (a [x] (b [x] c)),b <> {} by A8, CAT_1:52;
A13: Hom (a [x] (b [x] c)),a <> {} by Th21;
then A14: Hom (a [x] (b [x] c)),(a [x] b) <> {} by A12, Th25;
A15: Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} by Th38;
then ((pr2 a,b) * (pr1 (a [x] b),c)) * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):> = (pr2 a,b) * ((pr1 (a [x] b),c) * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):>) by A1, A2, CAT_1:54
.= (pr2 a,b) * <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):> by A10, A14, Def11
.= (pr1 b,c) * (pr2 a,(b [x] c)) by A12, A13, Def11 ;
then A16: <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):> * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):> = <:((pr1 b,c) * (pr2 a,(b [x] c))),((pr2 (a [x] b),c) * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):>):> by A3, A4, A15, Th27
.= <:((pr1 b,c) * (pr2 a,(b [x] c))),((pr2 b,c) * (pr2 a,(b [x] c))):> by A10, A14, Def11
.= <:(pr1 b,c),(pr2 b,c):> * (pr2 a,(b [x] c)) by A11, A8, A9, Th27
.= (id (b [x] c)) * (pr2 a,(b [x] c)) by Th26
.= pr2 a,(b [x] c) by A8, CAT_1:57 ;
A17: Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} by Th38;
then ((pr1 b,c) * (pr2 a,(b [x] c))) * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:> = (pr1 b,c) * ((pr2 a,(b [x] c)) * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:>) by A11, A8, CAT_1:54
.= (pr1 b,c) * <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):> by A7, A5, Def11
.= (pr2 a,b) * (pr1 (a [x] b),c) by A3, A4, Def11 ;
then A18: <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):> * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:> = <:((pr1 a,(b [x] c)) * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:>),((pr2 a,b) * (pr1 (a [x] b),c)):> by A17, A12, A13, Th27
.= <:((pr1 a,b) * (pr1 (a [x] b),c)),((pr2 a,b) * (pr1 (a [x] b),c)):> by A7, A5, Def11
.= <:(pr1 a,b),(pr2 a,b):> * (pr1 (a [x] b),c) by A6, A1, A2, Th27
.= (id (a [x] b)) * (pr1 (a [x] b),c) by Th26
.= pr1 (a [x] b),c by A1, CAT_1:57 ;
((pr1 a,b) * (pr1 (a [x] b),c)) * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):> = (pr1 a,b) * ((pr1 (a [x] b),c) * <:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):>) by A6, A1, A15, CAT_1:54
.= (pr1 a,b) * <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):> by A10, A14, Def11
.= pr1 a,(b [x] c) by A12, A13, Def11 ;
hence (Alpha a,b,c) * (Alpha' a,b,c) = <:(pr1 a,(b [x] c)),(pr2 a,(b [x] c)):> by A7, A5, A15, A16, Th27
.= id (a [x] (b [x] c)) by Th26 ;
:: thesis: (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c)
((pr2 b,c) * (pr2 a,(b [x] c))) * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:> = (pr2 b,c) * ((pr2 a,(b [x] c)) * <:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:>) by A17, A8, A9, CAT_1:54
.= (pr2 b,c) * <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):> by A7, A5, Def11
.= pr2 (a [x] b),c by A3, A4, Def11 ;
hence (Alpha' a,b,c) * (Alpha a,b,c) = <:(pr1 (a [x] b),c),(pr2 (a [x] b),c):> by A17, A10, A14, A18, Th27
.= id ((a [x] b) [x] c) by Th26 ;
:: thesis: verum