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) * (1_minus g)) by FUNCT_2:def 1;
A2: 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 5
.= (1 - (f . c)) * (1 - (g . c)) by FUZZY_1:def 5
.= 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 5; :: thesis: verum

end;

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