let C be non empty set ; :: thesis: ( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C )
A1: for x being Element of C st x in C holds
(1_minus (EMF C)) . x = (UMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x )
(1_minus (EMF C)) . x = 1 - ((EMF C) . x) by Def5
.= 1 - 0 by FUNCT_3:def 3
.= 1 ;
hence ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x ) by FUNCT_3:def 3; :: thesis: verum

end;

( C = dom (1_minus (EMF C)) & C = dom (UMF C) ) by FUNCT_2:def 1;
hence 1_minus (EMF C) = UMF C by A1, PARTFUN1:5; :: thesis: 1_minus (UMF C) = EMF C
A2: for x being Element of C st x in C holds
(1_minus (UMF C)) . x = (EMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x )
(1_minus (UMF C)) . x = 1 - ((UMF C) . x) by Def5
.= 1 - 1 by FUNCT_3:def 3
.= 0 ;
hence ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x ) by FUNCT_3:def 3; :: thesis: verum

end;

( C = dom (1_minus (UMF C)) & C = dom (EMF C) ) by FUNCT_2:def 1;
hence 1_minus (UMF C) = EMF C by A2, PARTFUN1:5; :: thesis: verum