let a, b, c, d be Real; for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))
let f be Function of REAL,REAL; ( b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c))) )
assume A1:
( b > 0 & c > 0 & d > 0 & d < b )
; ( ex x being Real st not f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) or f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c))) )
assume A2:
for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))
; f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))
A3: dom f =
REAL
by FUNCT_2:def 1
.=
dom (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c))))
by FUNCT_2:def 1
;
for x being object st x in dom f holds
f . x = (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x
proof
let x be
object ;
( x in dom f implies f . x = (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x )
assume
x in dom f
;
f . x = (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x
then reconsider x =
x as
Real ;
f . x =
min (
d,
(max (0,(b - |.((b * (x - a)) / c).|))))
by A2
.=
(d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x
by A1, LmCri2
;
hence
f . x = (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x
;
verum
end;
hence
f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))
by A3, FUNCT_1:2; verum