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: dom (1r (#) f) = dom f by Th7;

now

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 Th7
.= f /. c by COMPLEX1:def 7 ;
:: thesis: verum

end;

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