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

(f * (EMF C)) . c = (EMF C) . c

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

( 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

A4:
for c being Element of C st c in C holds
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;(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

(f * (EMF C)) . c = (EMF C) . c

proof

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

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