let a, b, c be Real; :: thesis:
let f be Function of REAL,REAL; :: thesis:
assume A1: b > 0 ; :: thesis:
assume A2: c > 0 ; :: thesis:
assume A3: for x being Real holds f . x = b - |.((b * (x - a)) / c).| ; :: thesis:
INF: ( -infty < a & a < +infty ) by XXREAL_0:9, XXREAL_0:12, XREAL_0:def 1;
D1a: dom (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) = (dom ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.])) \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) by FUNCT_4:def 1
.= ].-infty,a.] \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) by FUNCT_2:def 1
.= ].-infty,a.] \/ [.a,+infty.[ by FUNCT_2:def 1
.= ].-infty,+infty.[ by XXREAL_1:172, INF ;
for x being object st x in dom f holds
f . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x

let x be object ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider x = x as Element of REAL ;
f . x = b - |.((b * (x - a)) / c).| by A3;
hence f . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x by Th1, A1, A2; :: thesis:

end;