let C be non empty set ; :: thesis: for f, g being Membership_Func of C st f \ g = EMF C holds

g c=

let f, g be Membership_Func of C; :: thesis: ( f \ g = EMF C implies g c= )

assume A1: f \ g = EMF C ; :: thesis: g c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . c <= g . c

A2: min ((f . c),((1_minus g) . c)) = (EMF C) . c by A1, FUZZY_1:5;

g c=

let f, g be Membership_Func of C; :: thesis: ( f \ g = EMF C implies g c= )

assume A1: f \ g = EMF C ; :: thesis: g c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . c <= g . c

A2: min ((f . c),((1_minus g) . c)) = (EMF C) . c by A1, FUZZY_1:5;