let C be non empty set ; :: thesis: for f being Membership_Func of C holds
( f * (EMF C) = EMF C & f * (UMF C) = f )
let f be Membership_Func of C; :: thesis: ( f * (EMF C) = EMF C & f * (UMF C) = f )
A1: f * (EMF C) = EMF C

proof

A2: ( C = dom (EMF C) & C = dom (f * (EMF C)) ) by FUNCT_2:def 1;
for c being Element of C st c in C holds
(f * (EMF C)) . c = (EMF C) . c

proof

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

end;

hence f * (EMF C) = EMF C by A2, PARTFUN1:34; :: thesis: verum

end;

f * (UMF C) = f

proof

A3: ( C = dom f & C = dom (f * (UMF C)) ) by FUNCT_2:def 1;
for c being Element of C st c in C holds
(f * (UMF C)) . c = f . c

proof

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

end;

hence f * (UMF C) = f by A3, PARTFUN1:34; :: thesis: verum

end;

hence ( f * (EMF C) = EMF C & f * (UMF C) = f ) by A1; :: thesis: verum