per cases ( k in dom s or not k in dom s ) ;

suppose A1: k in dom s ; :: thesis: s . k is Element of COMPLEX

A2: rng s c= COMPLEX by VALUED_0:def 1;
s . k in rng s by A1, FUNCT_1:def 3;
hence s . k is Element of COMPLEX by A2; :: thesis: verum

end;

suppose not k in dom s ; :: thesis: s . k is Element of COMPLEX

then s . k = 0c by FUNCT_1:def 2;
hence s . k is Element of COMPLEX ; :: thesis: verum

end;

end;