defpred S_{1}[ 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_{1}[x,y,z]

A3: for x, y being Element of INT holds S_{1}[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

A1: for x, y being Element of INT ex z being Element of REAL st S

proof

consider f being Function of [:INT,INT:],REAL such that
let x, y be Element of INT ; :: thesis: ex z being Element of REAL st S_{1}[x,y,z]

((a0 * x) + (b0 * y)) + c0 in REAL by XREAL_0:def 1;

hence ex z being Element of REAL st S_{1}[x,y,z]
; :: thesis: verum

end;((a0 * x) + (b0 * y)) + c0 in REAL by XREAL_0:def 1;

hence ex z being Element of REAL st S

A3: for x, y being Element of INT holds S

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