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 A1: rng f c= X * ;
per cases ( x in dom f or not x in dom f ) ;
suppose A2: 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 A2;
reconsider ff = f as Function of D,(X *) by FUNCT_2:2, A1;
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;