let a, b, p, q be Real; for f being FuzzySet of REAL st a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) & ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
( f is trapezoidal & f is normalized )
let f be FuzzySet of REAL; ( a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) & ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) implies ( f is trapezoidal & f is normalized ) )
assume that
A1:
( a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) )
and
A2:
for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
; ( f is trapezoidal & f is normalized )
D1:
( REAL = dom f & REAL = dom (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) )
by FUNCT_2:52;
for x being object st x in dom f holds
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = f . x
proof
let x be
object ;
( x in dom f implies (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = f . x )
assume
x in dom f
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = f . x
then reconsider x =
x as
Real by D1;
f . x =
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by A2
.=
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x
by A1, asymTT7
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = f . x
;
verum
end;
then A4:
f = TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))
by FUNCT_1:2, D1;
( 0 + (- q) < 1 + (- q) & - p < 0 )
by A1, XREAL_1:8;
then A7:
(1 - q) / (- p) < (- q) / (- p)
by XREAL_1:75;
0 + (- b) < 1 + (- b)
by XREAL_1:8;
then
( (- b) / a < (1 - b) / a & (1 - b) / a < (1 - q) / (- p) & (1 - q) / (- p) < q / p )
by XREAL_1:74, A1, A7, XCMPLX_1:191;
hence
( f is trapezoidal & f is normalized )
by FUZNUM_1:31, A4; verum