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)) - (((1_minus f) . c) * ((1_minus g) . c)) by Def3
.= ((1 - (f . c)) + ((1_minus g) . c)) - (((1_minus f) . c) * ((1_minus g) . c)) by FUZZY_1:def 5
.= ((1 - (f . c)) + (1 - (g . c))) - (((1_minus f) . c) * ((1_minus g) . c)) by FUZZY_1:def 5
.= ((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * ((1_minus g) . c)) by FUZZY_1:def 5
.= ((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * (1 - (g . c))) by FUZZY_1:def 5
.= (((g . c) - (g . c)) + 1) - ((f . c) * (g . c))
.= 1 - ((f * g) . c) by Def2 ;
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