let C be CategoryStr ; :: thesis: ( C is associative iff C opp is associative )

hereby :: thesis: ( C opp is associative implies C is associative )

assume A1: C is associative ; :: thesis: C opp is associative
for g1, g2, g3 being morphism of (C opp) st g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 holds
g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

proof

let g1, g2, g3 be morphism of (C opp); :: thesis: ( g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 implies g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
reconsider f3 = g1, f2 = g2, f1 = g3 as morphism of C ;
assume g1 |> g2 ; :: thesis: ( not g2 |> g3 or not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then A2: f2 |> f3 by FUNCT_4:42;
assume g2 |> g3 ; :: thesis: ( not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then A3: f1 |> f2 by FUNCT_4:42;
assume A4: g1 (*) g2 |> g3 ; :: thesis: ( not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
assume A5: g1 |> g2 (*) g3 ; :: thesis: g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
A6: g1 (*) g2 = f2 (*) f3 by A2, Th3;
then A7: f1 |> f2 (*) f3 by A4, FUNCT_4:42;
A8: f1 (*) f2 = g2 (*) g3 by A3, Th3;
then A9: f1 (*) f2 |> f3 by A5, FUNCT_4:42;
thus g1 (*) (g2 (*) g3) = (f1 (*) f2) (*) f3 by A8, A9, Th3
.= f1 (*) (f2 (*) f3) by A1, A2, A3, A7, A9
.= (g1 (*) g2) (*) g3 by A6, A7, Th3 ; :: thesis: verum

end;

hence C opp is associative ; :: thesis: verum

end;

assume A10: C opp is associative ; :: thesis: C is associative
for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3

proof

let f1, f2, f3 be morphism of C; :: thesis: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 implies f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
reconsider g3 = f1, g2 = f2, g1 = f3 as morphism of (C opp) ;
assume A11: f1 |> f2 ; :: thesis: ( not f2 |> f3 or not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
then A12: g2 |> g3 by FUNCT_4:42;
assume A13: f2 |> f3 ; :: thesis: ( not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
then A14: g1 |> g2 by FUNCT_4:42;
assume A15: f1 (*) f2 |> f3 ; :: thesis: ( not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A16: f1 |> f2 (*) f3 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
A17: f1 (*) f2 = g2 (*) g3 by A11, Th3;
then A18: g1 |> g2 (*) g3 by A15, FUNCT_4:42;
A19: g1 (*) g2 = f2 (*) f3 by A13, Th3;
then A20: g1 (*) g2 |> g3 by A16, FUNCT_4:42;
thus f1 (*) (f2 (*) f3) = (g1 (*) g2) (*) g3 by A19, A16, Th3
.= g1 (*) (g2 (*) g3) by A10, A12, A14, A18, A20
.= (f1 (*) f2) (*) f3 by A17, A15, Th3 ; :: thesis: verum

end;

hence C is associative ; :: thesis: verum