let o1, o2 be BinOp of (LinComb V); ( ( for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ) implies o1 = o2 )
assume A2:
for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2)
; ( ex e1, e2 being Element of LinComb V st not o2 . (e1,e2) = (@ e1) + (@ e2) or o1 = o2 )
assume A3:
for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2)
; o1 = o2
hence
o1 = o2
; verum