deffunc H₁( object , object ) -> Complex = subtraction ($1,$2);
A2: for x, y being object st x in A & y in A holds
subtraction (x,y) in A

proof

let x, y be object ; :: thesis: ( x in A & y in A implies subtraction (x,y) in A )
assume ( x in A & y in A ) ; :: thesis: subtraction (x,y) in A
subtraction (x,y) in COMPLEX by XCMPLX_0:def 2;
hence subtraction (x,y) in A by A1; :: thesis: verum

end;

consider f being Function of [:A,A:],A such that
A3: for x, y being object st x in A & y in A holds
f . (x,y) = subtraction (x,y) from BINOP_1:sch 2(A2);
take f ; :: thesis: for x, y being object st x in A & y in A holds
f . (x,y) = subtraction (x,y)
thus for x, y being object st x in A & y in A holds
f . (x,y) = subtraction (x,y) by A3; :: thesis: verum