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) )
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;
A4: Hom (a [x] b),b <> {} by Th21;
then A5: Hom ((a [x] b) [x] c),b <> {} by A2, CAT_1:52;
A6: Hom ((a [x] b) [x] c),c <> {} by Th21;
then A7: Hom ((a [x] b) [x] c),(b [x] c) <> {} by A5, Th25;
A8: Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} by Th38;
A9: Hom (b [x] c),b <> {} by Th21;
A10: Hom (a [x] (b [x] c)),(b [x] c) <> {} by Th21;
then A11: Hom (a [x] (b [x] c)),b <> {} by A9, CAT_1:52;
A12: Hom (b [x] c),c <> {} by Th21;
then A13: Hom (a [x] (b [x] c)),c <> {} by A10, CAT_1:52;
A14: Hom (a [x] (b [x] c)),a <> {} by Th21;
then A15: Hom (a [x] (b [x] c)),(a [x] b) <> {} by A11, Th25;
A16: Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} by Th38;
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))):>;
A17: ((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 A1, A2, A16, CAT_1:54
.= (pr1 a,b) * <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):> by A13, A15, Def11
.= pr1 a,(b [x] c) by A11, A14, Def11 ;
((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 A2, A4, A16, CAT_1:54
.= (pr2 a,b) * <:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):> by A13, A15, Def11
.= (pr1 b,c) * (pr2 a,(b [x] c)) by A11, A14, Def11 ;
then <:((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 A5, A6, A16, Th27
.= <:((pr1 b,c) * (pr2 a,(b [x] c))),((pr2 b,c) * (pr2 a,(b [x] c))):> by A13, A15, Def11
.= <:(pr1 b,c),(pr2 b,c):> * (pr2 a,(b [x] c)) by A9, A10, A12, Th27
.= (id (b [x] c)) * (pr2 a,(b [x] c)) by Th26
.= pr2 a,(b [x] c) by A10, CAT_1:57 ;
hence (Alpha a,b,c) * (Alpha' a,b,c) = <:(pr1 a,(b [x] c)),(pr2 a,(b [x] c)):> by A3, A7, A16, A17, Th27
.= id (a [x] (b [x] c)) by Th26 ;
:: thesis: (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] 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 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 A8, A9, A10, CAT_1:54
.= (pr1 b,c) * <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):> by A3, A7, Def11
.= (pr2 a,b) * (pr1 (a [x] b),c) by A5, A6, 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 A8, A11, A14, Th27
.= <:((pr1 a,b) * (pr1 (a [x] b),c)),((pr2 a,b) * (pr1 (a [x] b),c)):> by A3, A7, Def11
.= <:(pr1 a,b),(pr2 a,b):> * (pr1 (a [x] b),c) by A1, A2, A4, Th27
.= (id (a [x] b)) * (pr1 (a [x] b),c) by Th26
.= pr1 (a [x] b),c by A2, CAT_1:57 ;
((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 A8, A10, A12, CAT_1:54
.= (pr2 b,c) * <:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):> by A3, A7, Def11
.= pr2 (a [x] b),c by A5, A6, Def11 ;
hence (Alpha' a,b,c) * (Alpha a,b,c) = <:(pr1 (a [x] b),c),(pr2 (a [x] b),c):> by A8, A13, A15, A18, Th27
.= id ((a [x] b) [x] c) by Th26 ;
:: thesis: verum