let f be Function of REAL,REAL; :: thesis: for a, b, c being Real st ( for x being Real holds f . x = b - |.((b * (x - a)) / c).| ) holds
for y being Real holds f . (a - y) = f . (a + y)
let a, b, c be Real; :: thesis: ( ( for x being Real holds f . x = b - |.((b * (x - a)) / c).| ) implies for y being Real holds f . (a - y) = f . (a + y) )
assume A2: for x being Real holds f . x = b - |.((b * (x - a)) / c).| ; :: thesis: for y being Real holds f . (a - y) = f . (a + y)
let y be Real; :: thesis: f . (a - y) = f . (a + y)
thus f . (a - y) = b - |.((b * ((a - y) - a)) / c).| by A2
.= b - |.((- (y * b)) * (1 / c)).| by XCMPLX_1:99
.= b - |.(- ((y * b) * (1 / c))).|
.= b - |.(- ((y * b) / c)).| by XCMPLX_1:99
.= b - |.((b * ((a + y) - a)) / c).| by COMPLEX1:52
.= f . (a + y) by A2 ; :: thesis: verum