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

A1: now

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 Def4
.= f /. c by CLVECT_1:def 5 ;
:: thesis: verum

end;

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