let C be non empty set ; :: thesis: for f being Membership_Func of C holds
( f ++ (EMF C) = f & f ++ (UMF C) = UMF C )
let f be Membership_Func of C; :: thesis: ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C )
A1: C = dom (f ++ (EMF C)) by FUNCT_2:def 1;
A2: C = dom (UMF C) by FUNCT_2:def 1;
A3: for c being Element of C st c in C holds
(f ++ (UMF C)) . c = (UMF C) . c

proof

let c be Element of C; :: thesis: ( c in C implies (f ++ (UMF C)) . c = (UMF C) . c )
(f ++ (UMF C)) . c = ((f . c) + ((UMF C) . c)) - ((f . c) * ((UMF C) . c)) by Def3
.= (((UMF C) . c) + (f . c)) - ((f . c) * 1) by FUNCT_3:def 3
.= ((UMF C) . c) + ((f . c) - (f . c)) ;
hence ( c in C implies (f ++ (UMF C)) . c = (UMF C) . c ) ; :: thesis: verum

end;

A4: for c being Element of C st c in C holds
(f ++ (EMF C)) . c = f . c

proof

let c be Element of C; :: thesis: ( c in C implies (f ++ (EMF C)) . c = f . c )
(f ++ (EMF C)) . c = ((f . c) + ((EMF C) . c)) - ((f . c) * ((EMF C) . c)) by Def3
.= ((f . c) + 0) - ((f . c) * ((EMF C) . c)) by FUNCT_3:def 3
.= (f . c) - ((f . c) * 0) by FUNCT_3:def 3 ;
hence ( c in C implies (f ++ (EMF C)) . c = f . c ) ; :: thesis: verum

end;

A5: C = dom (f ++ (UMF C)) by FUNCT_2:def 1;
C = dom f by FUNCT_2:def 1;
hence ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C ) by A1, A4, A2, A5, A3, PARTFUN1:5; :: thesis: verum