let a, b be Real; :: thesis: ( b <> 0 implies { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } c= Membership_Funcs REAL )

assume A0: b <> 0 ; :: thesis: { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } c= Membership_Funcs REAL

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } or y in Membership_Funcs REAL )

assume y in { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } ; :: thesis: y in Membership_Funcs REAL

then consider f being Function of REAL,REAL such that

A1: y = f and

A2: for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ;

f is FuzzySet of REAL by A0, A2, GauF04complex;

hence y in Membership_Funcs REAL by Def1, A1; :: thesis: verum

assume A0: b <> 0 ; :: thesis: { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } c= Membership_Funcs REAL

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } or y in Membership_Funcs REAL )

assume y in { f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } ; :: thesis: y in Membership_Funcs REAL

then consider f being Function of REAL,REAL such that

A1: y = f and

A2: for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ;

f is FuzzySet of REAL by A0, A2, GauF04complex;

hence y in Membership_Funcs REAL by Def1, A1; :: thesis: verum