let f, f9 be Function of REAL,REAL; ( ( for x being Real holds f . x = (a * x) + b ) & ( for x being Real holds f9 . x = (a * x) + b ) implies f = f9 )
assume that
A2:
for x being Real holds f . x = (a * x) + b
and
A3:
for x being Real holds f9 . x = (a * x) + b
; f = f9
hence
f = f9
by FUNCT_2:63; verum