now :: thesis: for o being object st o in X holds
((1. R) '*' f) . o = f . o

let o be object ; :: thesis: ( o in X implies ((1. R) '*' f) . o = f . o )
assume o in X ; :: thesis: ((1. R) '*' f) . o = f . o
then reconsider x = o as Element of X ;
thus ((1. R) '*' f) . o = (1. R) * (f . x) by defmu
.= f . o by VECTSP_1:def 17 ; :: thesis: verum

end;

hence (1. R) '*' f = f by FUNCT_2:12; :: thesis: verum