let f, g be MorphismsFamily of EnsCatProductObj A,A; :: thesis: ( ( for i being set st i in I holds
f . i = proj (A,i) ) & ( for i being set st i in I holds
g . i = proj (A,i) ) implies f = g )
assume that
A7: for i being set st i in I holds
f . i = proj (A,i) and
A8: for i being set st i in I holds
g . i = proj (A,i) ; :: thesis: f = g

now :: thesis: for i being object st i in I holds
f . i = g . i

let i be object ; :: thesis: ( i in I implies f . i = g . i )
assume A9: i in I ; :: thesis: f . i = g . i
hence f . i = proj (A,i) by A7
.= g . i by A8, A9 ;
:: thesis: verum

end;

hence f = g by PBOOLE:3; :: thesis: verum