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: C = dom (f * (EMF C)) by FUNCT_2:def 1;
A2: C = dom f by FUNCT_2:def 1;
A3: 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;

A4: 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;

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