let C1, C2 be non empty category; :: thesis: for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st [f1,f2] = [g1,g2] holds
( f1 = g1 & f2 = g2 )
let f1, g1 be morphism of C1; :: thesis: for f2, g2 being morphism of C2 st [f1,f2] = [g1,g2] holds
( f1 = g1 & f2 = g2 )
let f2, g2 be morphism of C2; :: thesis: ( [f1,f2] = [g1,g2] implies ( f1 = g1 & f2 = g2 ) )
assume A1: [f1,f2] = [g1,g2] ; :: thesis: ( f1 = g1 & f2 = g2 )
( (pr1 (C1,C2)) . [f1,f2] = f1 & (pr1 (C1,C2)) . [g1,g2] = g1 ) by Def23;
hence f1 = g1 by A1; :: thesis: f2 = g2
( (pr2 (C1,C2)) . [f1,f2] = f2 & (pr2 (C1,C2)) . [g1,g2] = g2 ) by Def23;
hence f2 = g2 by A1; :: thesis: verum