let a, b, p, q be Real; :: thesis: 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; :: thesis: ( 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)))) ; :: thesis: ( 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 ; :: thesis: ( x in dom f implies (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = f . x )
assume x in dom f ; :: thesis: (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 ; :: thesis: 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; :: thesis: verum