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

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