let f, g be BinOp of (setvect M); :: thesis: ( ( for u1, v1 being Element of setvect M holds f . u1,v1 = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds g . u1,v1 = u1 + v1 ) implies f = g )
assume that
A3: for u1, v1 being Element of setvect M holds f . u1,v1 = u1 + v1 and
A4: for u1, v1 being Element of setvect M holds g . u1,v1 = u1 + v1 ; :: thesis: f = g
for u1, v1 being Element of setvect M holds f . u1,v1 = g . u1,v1

proof

let u1, v1 be Element of setvect M; :: thesis: f . u1,v1 = g . u1,v1
f . u1,v1 = u1 + v1 by A3;
hence f . u1,v1 = g . u1,v1 by A4; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum