let C be non empty set ; :: thesis: for f being Membership_Func of C holds
( f c= & f ++ f c= )
let f be Membership_Func of C; :: thesis: ( f c= & f ++ f c= )
thus f c= :: thesis: f ++ f c=

proof

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f * f) . c <= f . c
A1: 0 <= f . c by Th1;
f . c <= 1 by Th1;
then (f . c) * (f . c) <= 1 * (f . c) by A1, XREAL_1:64;
hence (f * f) . c <= f . c by Def2; :: thesis: verum

end;

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . c <= (f ++ f) . c
A2: 0 <= f . c by Th1;
0 <= (1_minus f) . c by Th1;
then 0 * (f . c) <= (f . c) * ((1_minus f) . c) by A2, XREAL_1:64;
then 0 <= (f . c) * (1 - (f . c)) by FUZZY_1:def 5;
then 0 + (f . c) <= ((f . c) - ((f . c) * (f . c))) + (f . c) by XREAL_1:6;
then f . c <= ((f . c) + (f . c)) - ((f . c) * (f . c)) ;
hence f . c <= (f ++ f) . c by Def3; :: thesis: verum