deffunc H₁( Element of AFV, Element of AFV) -> Element of AFV = Padd o,$1,$2;
consider O being BinOp of the carrier of AFV such that
A1: for a, b being Element of AFV holds O . a,b = H₁(a,b) from BINOP_1:sch 4();
take O ; :: thesis: for a, b being Element of AFV holds O . a,b = Padd o,a,b
thus for a, b being Element of AFV holds O . a,b = Padd o,a,b by A1; :: thesis: verum