deffunc H₁( Element of LinComb V, Element of LinComb V) -> Element of LinComb V = @ ((@ $1) + (@ $2));
consider o being BinOp of (LinComb V) such that
A1: for e1, e2 being Element of LinComb V holds o . (e1,e2) = H₁(e1,e2) from BINOP_1:sch 4();
take o ; :: thesis: for e1, e2 being Element of LinComb V holds o . (e1,e2) = (@ e1) + (@ e2)
let e1, e2 be Element of LinComb V; :: thesis: o . (e1,e2) = (@ e1) + (@ e2)
thus o . (e1,e2) = @ ((@ e1) + (@ e2)) by A1
.= (@ e1) + (@ e2) ; :: thesis: verum