let o1, o2 be BinOp of (LinComb V); :: thesis: ( ( 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) ; :: thesis: ( 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) ; :: thesis: o1 = o2

now :: thesis: for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = o2 . (e1,e2)

let e1, e2 be Element of LinComb V; :: thesis: o1 . (e1,e2) = o2 . (e1,e2)
thus o1 . (e1,e2) = (@ e1) + (@ e2) by A2
.= o2 . (e1,e2) by A3 ; :: thesis: verum

end;

hence o1 = o2 ; :: thesis: verum