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