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