let F1, F2 be Function of [:INT,INT:],REAL; :: thesis: ( ( for x, y being Integer holds F1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) & ( for x, y being Integer holds F2 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) implies F1 = F2 )

assume that

A4: for x, y being Integer holds F1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 and

A5: for x, y being Integer holds F2 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ; :: thesis: F1 = F2

assume that

A4: for x, y being Integer holds F1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 and

A5: for x, y being Integer holds F2 . (x,y) = ((a0 * x) + (b0 * y)) + c0 ; :: thesis: F1 = F2

now :: thesis: for x, y being Element of INT holds F1 . (x,y) = F2 . (x,y)

hence
F1 = F2
by BINOP_1:2; :: thesis: verumlet x, y be Element of INT ; :: thesis: F1 . (x,y) = F2 . (x,y)

thus F1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 by A4

.= F2 . (x,y) by A5 ; :: thesis: verum

end;thus F1 . (x,y) = ((a0 * x) + (b0 * y)) + c0 by A4

.= F2 . (x,y) by A5 ; :: thesis: verum