let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st ( 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 FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( ( 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 FuzzySet of REAL )
assume A3: 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 FuzzySet of REAL
set g = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[);
reconsider g = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) as Function of REAL,REAL by asymTT10;
for x being Real holds f . x = max (0,(min (1,(g . x)))) by A3;
hence f is FuzzySet of REAL by MM40; :: thesis: verum