let C be non empty set ; :: thesis: for V being non empty scalar-unital RLSStruct
for f being PartFunc of C,V holds 1 (#) f = f
let V be non empty scalar-unital RLSStruct ; :: thesis: for f being PartFunc of C,V holds 1 (#) f = f
let f be PartFunc of C,V; :: thesis: 1 (#) f = f

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

let c be Element of C; :: thesis: ( c in dom (1 (#) f) implies (1 (#) f) /. c = f /. c )
assume c in dom (1 (#) f) ; :: thesis: (1 (#) f) /. c = f /. c
hence (1 (#) f) /. c = 1 * (f /. c) by Def4
.= f /. c by RLVECT_1:def 8 ;
:: thesis: verum

end;

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