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 Th19;
A2: Hom ((a [x] b),b) <> {} by Th19;
then A3: Hom (((a [x] b) [x] c),b) <> {} by A1, CAT_1:24;
A4: Hom (((a [x] b) [x] c),c) <> {} by Th19;
then A5: Hom (((a [x] b) [x] c),(b [x] c)) <> {} by A3, Th23;
A6: Hom ((a [x] b),a) <> {} by Th19;
then A7: Hom (((a [x] b) [x] c),a) <> {} by A1, CAT_1:24;
A8: Hom ((a [x] (b [x] c)),(b [x] c)) <> {} by Th19;
A9: Hom ((b [x] c),c) <> {} by Th19;
then A10: Hom ((a [x] (b [x] c)),c) <> {} by A8, CAT_1:24;
A11: Hom ((b [x] c),b) <> {} by Th19;
then A12: Hom ((a [x] (b [x] c)),b) <> {} by A8, CAT_1:24;
A13: Hom ((a [x] (b [x] c)),a) <> {} by Th19;
then A14: Hom ((a [x] (b [x] c)),(a [x] b)) <> {} by A12, Th23;
A15: Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} by Th36;
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:25
.= (pr2 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10
.= (pr1 (b,c)) * (pr2 (a,(b [x] c))) by A12, A13, Def10 ;
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, Th25
.= <:((pr1 (b,c)) * (pr2 (a,(b [x] c)))),((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10
.= <:(pr1 (b,c)),(pr2 (b,c)):> * (pr2 (a,(b [x] c))) by A11, A8, A9, Th25
.= (id (b [x] c)) * (pr2 (a,(b [x] c))) by Th24
.= pr2 (a,(b [x] c)) by A8, CAT_1:28 ;
A17: Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} by Th36;
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:25
.= (pr1 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> by A7, A5, Def10
.= (pr2 (a,b)) * (pr1 ((a [x] b),c)) by A3, A4, Def10 ;
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, Th25
.= <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),((pr2 (a,b)) * (pr1 ((a [x] b),c))):> by A7, A5, Def10
.= <:(pr1 (a,b)),(pr2 (a,b)):> * (pr1 ((a [x] b),c)) by A6, A1, A2, Th25
.= (id (a [x] b)) * (pr1 ((a [x] b),c)) by Th24
.= pr1 ((a [x] b),c) by A1, CAT_1:28 ;
((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:25
.= (pr1 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10
.= pr1 (a,(b [x] c)) by A12, A13, Def10 ;
hence (Alpha (a,b,c)) * (Alpha' (a,b,c)) = <:(pr1 (a,(b [x] c))),(pr2 (a,(b [x] c))):> by A7, A5, A15, A16, Th25
.= id (a [x] (b [x] c)) by Th24 ;
:: 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:25
.= (pr2 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> by A7, A5, Def10
.= pr2 ((a [x] b),c) by A3, A4, Def10 ;
hence (Alpha' (a,b,c)) * (Alpha (a,b,c)) = <:(pr1 ((a [x] b),c)),(pr2 ((a [x] b),c)):> by A17, A10, A14, A18, Th25
.= id ((a [x] b) [x] c) by Th24 ;
:: thesis: verum