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

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

end;

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