let C be CategoryStr ; :: thesis: for f1, f2 being morphism of C
for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g2 (*) g1
let f1, f2 be morphism of C; :: thesis: for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g2 (*) g1
let g1, g2 be morphism of (C opp); :: thesis: ( f1 = g1 & f2 = g2 & f1 |> f2 implies f1 (*) f2 = g2 (*) g1 )
assume A1: ( f1 = g1 & f2 = g2 ) ; :: thesis: ( not f1 |> f2 or f1 (*) f2 = g2 (*) g1 )
assume A2: f1 |> f2 ; :: thesis: f1 (*) f2 = g2 (*) g1
A3: g2 |> g1 by A1, A2, FUNCT_4:42;
thus f1 (*) f2 = the composition of C . (f1,f2) by A2, Def3
.= (~ the composition of C) . (f2,f1) by A2, FUNCT_4:def 2
.= g2 (*) g1 by A1, A3, Def3 ; :: thesis: verum