let X, x be set ; :: thesis: for f being Function st f is X * -valued holds
f . x in X *
let f be Function; :: thesis: ( f is X * -valued implies f . x in X * )
assume f is X * -valued ; :: thesis: f . x in X *
then B0: rng f c= X * by RELAT_1:def 19;

per cases ( x in dom f or not x in dom f ) ;

suppose C0: x in dom f ; :: thesis: f . x in X *

then reconsider D = dom f as non empty set ;
reconsider e = x as Element of D by C0;
reconsider ff = f as Function of D,(X *) by B0, FUNCT_2:2;
ff . e is Element of X * ;
hence f . x in X * ; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f . x in X *

then f . x = {} by FUNCT_1:def 2;
hence f . x in X * by FINSEQ_1:49; :: thesis: verum

end;

end;