let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds f ++ g = 1_minus ((1_minus f) * (1_minus g))
let f, g be Membership_Func of C; :: thesis: f ++ g = 1_minus ((1_minus f) * (1_minus g))
A1: C = dom (1_minus ((1_minus f) * (1_minus g))) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds
(f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c

proof

let c be Element of C; :: thesis: ( c in C implies (f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c )
(1_minus ((1_minus f) * (1_minus g))) . c = 1 - (((1_minus f) * (1_minus g)) . c) by FUZZY_1:def 5
.= 1 - (((1_minus f) . c) * ((1_minus g) . c)) by Def2
.= 1 - ((1 - (f . c)) * ((1_minus g) . c)) by FUZZY_1:def 5
.= 1 - ((1 - (f . c)) * (1 - (g . c))) by FUZZY_1:def 5
.= ((f . c) + (g . c)) - ((f . c) * (g . c)) ;
hence ( c in C implies (f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c ) by Def3; :: thesis: verum

end;

C = dom (f ++ g) by FUNCT_2:def 1;
hence f ++ g = 1_minus ((1_minus f) * (1_minus g)) by A1, A2, PARTFUN1:5; :: thesis: verum