let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds 1r (#) f = f
let f be PartFunc of C,COMPLEX; :: thesis: 1r (#) f = f

A1: now :: thesis: for c being Element of C st c in dom (1r (#) f) holds
(1r (#) f) /. c = f /. c

let c be Element of C; :: thesis: ( c in dom (1r (#) f) implies (1r (#) f) /. c = f /. c )
assume c in dom (1r (#) f) ; :: thesis: (1r (#) f) /. c = f /. c
hence (1r (#) f) /. c = 1r * (f /. c) by Th4
.= f /. c by COMPLEX1:def 4 ;
:: thesis: verum

end;

dom (1r (#) f) = dom f by Th4;
hence 1r (#) f = f by A1, PARTFUN2:1; :: thesis: verum