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 (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 Def5
.= 1 - (max ((f . x),(g . x))) by Def4
.= 1 - ((((f . x) + (g . x)) + |.((f . x) - (g . x)).|) / 2) by COMPLEX1:74 ;
(min ((1_minus f),(1_minus g))) . x = min (((1_minus f) . x),((1_minus g) . x)) by Def3
.= min ((1 - (f . x)),((1_minus g) . x)) by Def5
.= min ((1 - (f . x)),(1 - (g . x))) by Def5
.= (((1 - (f . x)) + (1 - (g . x))) - |.((1 - (f . x)) - (1 - (g . x))).|) / 2 by COMPLEX1:73
.= (((2 - (f . x)) - (g . x)) - |.(- ((f . x) - (g . x))).|) / 2
.= ((2 - ((f . x) + (g . x))) - |.((f . x) - (g . x)).|) / 2 by COMPLEX1:52
.= 1 - ((((f . x) + (g . x)) + |.((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;

A4: 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 )
A5: (1_minus (min (f,g))) . x = 1 - ((min (f,g)) . x) by Def5
.= 1 - (min ((f . x),(g . x))) by Def3
.= 1 - ((((f . x) + (g . x)) - |.((f . x) - (g . x)).|) / 2) by COMPLEX1:73 ;
(max ((1_minus f),(1_minus g))) . x = max (((1_minus f) . x),((1_minus g) . x)) by Def4
.= max ((1 - (f . x)),((1_minus g) . x)) by Def5
.= max ((1 - (f . x)),(1 - (g . x))) by Def5
.= (((1 - (f . x)) + (1 - (g . x))) + |.((1 - (f . x)) - (1 - (g . x))).|) / 2 by COMPLEX1:74
.= (((2 - (f . x)) - (g . x)) + |.(- ((f . x) - (g . x))).|) / 2
.= ((2 - ((f . x) + (g . x))) + |.((f . x) - (g . x)).|) / 2 by COMPLEX1:52
.= 1 - ((((f . x) + (g . x)) - |.((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 A5; :: thesis: verum

end;

( C = dom (1_minus (max (f,g))) & C = dom (min ((1_minus f),(1_minus g))) ) by FUNCT_2:def 1;
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, A4, PARTFUN1:5; :: thesis: verum