let f, f' be Function of REAL , REAL ; :: thesis: ( ( for x being real number holds f . x = (a * x) + b ) & ( for x being real number holds f' . x = (a * x) + b ) implies f = f' )
assume that
A2: for x being real number holds f . x = (a * x) + b and
A3: for x being real number holds f' . x = (a * x) + b ; :: thesis: f = f'

now

let x be Element of REAL ; :: thesis: f . x = f' . x
thus f . x = (a * x) + b by A2
.= f' . x by A3 ; :: thesis: verum

end;

hence f = f' by FUNCT_2:113; :: thesis: verum