let a, b be Real; :: thesis: for f being FuzzySet of REAL st b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds
f is triangular
let f be FuzzySet of REAL; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is triangular )
assume A1: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is triangular )
assume A2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is triangular
take a - b ; :: according to FUZNUM_1:def 9 :: thesis: not for b1, b2 being object holds R32( REAL , REAL ,f, TriangularFS ((a - b),b1,b2))
take a ; :: thesis: not for b1 being object holds R32( REAL , REAL ,f, TriangularFS ((a - b),a,b1))
take a + b ; :: thesis: R32( REAL , REAL ,f, TriangularFS ((a - b),a,(a + b)))
A4: ( dom (TriangularFS ((a - b),a,(a + b))) = REAL & dom f = REAL ) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = (TriangularFS ((a - b),a,(a + b))) . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = (TriangularFS ((a - b),a,(a + b))) . x )
assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x
then reconsider x = x as Real by A4;
f . x = max (0,(1 - |.((x - a) / b).|)) by A2
.= (TriangularFS ((a - b),a,(a + b))) . x by A1, TR6 ;
hence f . x = (TriangularFS ((a - b),a,(a + b))) . x ; :: thesis: verum
end;
hence R32( REAL , REAL ,f, TriangularFS ((a - b),a,(a + b))) by FUNCT_1:2, A4; :: thesis: verum