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)

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

hence
f = g
by BINOP_1:2; :: thesis: verum
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;f . (u1,v1) = u1 + v1 by A3;

hence f . (u1,v1) = g . (u1,v1) by A4; :: thesis: verum