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

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

let c be Element of M; :: 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 Def2
.= f /. c by CLVECT_1:def 5 ;
:: thesis: verum

end;

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