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

proof

let x be Element of C; :: thesis: ( x in C implies (1_minus (max f,g)) . x = (min (1_minus f),(1_minus g)) . x )
A3: (1_minus (max f,g)) . x = 1 - ((max f,g) . x) by Def6
.= 1 - (max (f . x),(g . x)) by Def5
.= 1 - ((((f . x) + (g . x)) + (abs ((f . x) - (g . x)))) / 2) by COMPLEX1:160 ;
(min (1_minus f),(1_minus g)) . x = min ((1_minus f) . x),((1_minus g) . x) by Def4
.= min (1 - (f . x)),((1_minus g) . x) by Def6
.= min (1 - (f . x)),(1 - (g . x)) by Def6
.= (((1 - (f . x)) + (1 - (g . x))) - (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:159
.= (((2 - (f . x)) - (g . x)) - (abs (- ((f . x) - (g . x))))) / 2
.= ((2 - ((f . x) + (g . x))) - (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:138
.= 1 - ((((f . x) + (g . x)) + (abs ((f . x) - (g . x)))) / 2) ;
hence ( x in C implies (1_minus (max f,g)) . x = (min (1_minus f),(1_minus g)) . x ) by A3; :: thesis: verum

end;

for x being Element of C st x in C holds
(1_minus (min f,g)) . x = (max (1_minus f),(1_minus g)) . x

proof

let x be Element of C; :: thesis: ( x in C implies (1_minus (min f,g)) . x = (max (1_minus f),(1_minus g)) . x )
A4: (1_minus (min f,g)) . x = 1 - ((min f,g) . x) by Def6
.= 1 - (min (f . x),(g . x)) by Def4
.= 1 - ((((f . x) + (g . x)) - (abs ((f . x) - (g . x)))) / 2) by COMPLEX1:159 ;
(max (1_minus f),(1_minus g)) . x = max ((1_minus f) . x),((1_minus g) . x) by Def5
.= max (1 - (f . x)),((1_minus g) . x) by Def6
.= max (1 - (f . x)),(1 - (g . x)) by Def6
.= (((1 - (f . x)) + (1 - (g . x))) + (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:160
.= (((2 - (f . x)) - (g . x)) + (abs (- ((f . x) - (g . x))))) / 2
.= ((2 - ((f . x) + (g . x))) + (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:138
.= 1 - ((((f . x) + (g . x)) - (abs ((f . x) - (g . x)))) / 2) ;
hence ( x in C implies (1_minus (min f,g)) . x = (max (1_minus f),(1_minus g)) . x ) by A4; :: thesis: verum

end;

hence ( 1_minus (max f,g) = min (1_minus f),(1_minus g) & 1_minus (min f,g) = max (1_minus f),(1_minus g) ) by A1, A2, PARTFUN1:34; :: thesis: verum