let X be RealUnitarySpace; :: thesis: for w being Point of X
for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X
let w be Point of X; :: thesis: for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X
let f be Function of X,REAL; :: thesis: ( ( for v being Point of X holds f . v = w .|. v ) implies f is_continuous_on the carrier of X )
assume AS: for v being Point of X holds f . v = w .|. v ; :: thesis: f is_continuous_on the carrier of X
set Y = RUSp2RNSp X;
reconsider g = f as Function of (RUSp2RNSp X),REAL ;
A3: dom g = the carrier of (RUSp2RNSp X) by FUNCT_2:def 1;
for y0 being Point of (RUSp2RNSp X) st y0 in the carrier of (RUSp2RNSp X) holds
g | the carrier of (RUSp2RNSp X) is_continuous_in y0 then g is_continuous_on the carrier of (RUSp2RNSp X) by FUNCT_2:def 1;
hence f is_continuous_on the carrier of X by LM3C; :: thesis: verum