defpred S₁[ Integer, Integer, set ] means $3 = ((a0 * $1) + (b0 * $2)) + c0;
A1: for x, y being Element of INT ex z being Element of REAL st S₁[x,y,z]

proof

let x, y be Element of INT ; :: thesis: ex z being Element of REAL st S₁[x,y,z]
((a0 * x) + (b0 * y)) + c0 in REAL by XREAL_0:def 1;
hence ex z being Element of REAL st S₁[x,y,z] ; :: thesis: verum

end;

consider f being Function of [:INT,INT:],REAL such that
A3: for x, y being Element of INT holds S₁[x,y,f . (x,y)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for x, y being Integer holds f . (x,y) = ((a0 * x) + (b0 * y)) + c0
let x, y be Integer; :: thesis: f . (x,y) = ((a0 * x) + (b0 * y)) + c0
( x in INT & y in INT ) by INT_1:def 2;
hence f . (x,y) = ((a0 * x) + (b0 * y)) + c0 by A3; :: thesis: verum