let f be Function of REAL,REAL; :: thesis: for a, b, c being Real st ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) holds

f is FuzzySet of REAL

let a, b, c be Real; :: thesis: ( ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) implies f is FuzzySet of REAL )

assume A2: for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ; :: thesis: f is FuzzySet of REAL

ex g being Function of REAL,REAL st

for x being Real holds g . x = c * (1 - |.((x - a) / b).|)

A4: for x being Real holds g . x = c * (1 - |.((x - a) / b).|) ;

for x being Real holds f . x = max (0,(min (1,(g . x))))

f is FuzzySet of REAL

let a, b, c be Real; :: thesis: ( ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) implies f is FuzzySet of REAL )

assume A2: for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ; :: thesis: f is FuzzySet of REAL

ex g being Function of REAL,REAL st

for x being Real holds g . x = c * (1 - |.((x - a) / b).|)

proof

then consider g being Function of REAL,REAL such that
deffunc H_{1}( Element of REAL ) -> Element of REAL = In ((c * (1 - |.(($1 - a) / b).|)),REAL);

consider f being Function of REAL,REAL such that

A1: for x being Element of REAL holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for x being Real holds f . x = c * (1 - |.((x - a) / b).|)

for x being Real holds f . x = c * (1 - |.((x - a) / b).|)

end;consider f being Function of REAL,REAL such that

A1: for x being Element of REAL holds f . x = H

take f ; :: thesis: for x being Real holds f . x = c * (1 - |.((x - a) / b).|)

for x being Real holds f . x = c * (1 - |.((x - a) / b).|)

proof

hence
for x being Real holds f . x = c * (1 - |.((x - a) / b).|)
; :: thesis: verum
let x be Real; :: thesis: f . x = c * (1 - |.((x - a) / b).|)

reconsider x = x as Element of REAL by XREAL_0:def 1;

f . x = H_{1}(x)
by A1;

hence f . x = c * (1 - |.((x - a) / b).|) ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

f . x = H

hence f . x = c * (1 - |.((x - a) / b).|) ; :: thesis: verum

A4: for x being Real holds g . x = c * (1 - |.((x - a) / b).|) ;

for x being Real holds f . x = max (0,(min (1,(g . x))))

proof

hence
f is FuzzySet of REAL
by MM40; :: thesis: verum
let x be Real; :: thesis: f . x = max (0,(min (1,(g . x))))

f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) by A2

.= max (0,(min (1,(g . x)))) by A4 ;

hence f . x = max (0,(min (1,(g . x)))) ; :: thesis: verum

end;f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) by A2

.= max (0,(min (1,(g . x)))) by A4 ;

hence f . x = max (0,(min (1,(g . x)))) ; :: thesis: verum