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