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

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

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

( 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

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 = (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;(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

(f ++ (EMF C)) . c = f . 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 = 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;(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

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