let C be non empty set ; :: thesis: for c being Element of C
for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c)))
let c be Element of C; :: thesis: for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c)))
let g, h be Membership_Func of C; :: thesis: (g ++ h) . c = 1 - ((1 - (g . c)) * (1 - (h . c)))
(g ++ h) . c = (1_minus ((1_minus g) * (1_minus h))) . c by Th36
.= 1 - (((1_minus g) * (1_minus h)) . c) by FUZZY_1:def 5
.= 1 - (((1_minus g) . c) * ((1_minus h) . c)) by Def2
.= 1 - ((1 - (g . c)) * ((1_minus h) . c)) by FUZZY_1:def 5 ;
hence (g ++ h) . c = 1 - ((1 - (g . c)) * (1 - (h . c))) by FUZZY_1:def 5; :: thesis: verum