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

proof

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

end;

hence 1_minus (f ++ g) = (1_minus f) * (1_minus g) by A1, PARTFUN1:34; :: thesis: verum