let F1, F2 be Function of [:INT,INT:],REAL; ( ( 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
; F1 = F2
now for x, y being Element of INT holds F1 . (x,y) = F2 . (x,y)let x,
y be
Element of
INT ;
F1 . (x,y) = F2 . (x,y)thus F1 . (
x,
y) =
((a0 * x) + (b0 * y)) + c0
by A4
.=
F2 . (
x,
y)
by A5
;
verum end;
hence
F1 = F2
by BINOP_1:2; verum