for x being object st x in dom ((<%> COMPLEX) ^ f) holds
((<%> COMPLEX) ^ f) . x is complex

proof

let x be object ; :: thesis: ( x in dom ((<%> COMPLEX) ^ f) implies ((<%> COMPLEX) ^ f) . x is complex )
assume A1: x in dom ((<%> COMPLEX) ^ f) ; :: thesis: ((<%> COMPLEX) ^ f) . x is complex
then reconsider x = x as Nat ;
A2: len (<%> COMPLEX) = 0 ;
then dom ((<%> COMPLEX) ^ f) = 0 + (len f) by Def1;
then x in Segm (len f) by A1;
then x + 1 in Seg (len f) by NEWTON02:106;
then x + 1 in dom f by FINSEQ_1:def 3;
then ((<%> COMPLEX) ^ f) . ((0 + (x + 1)) - 1) = f . (x + 1) by A2, Def1;
hence ((<%> COMPLEX) ^ f) . x is complex ; :: thesis: verum

end;

hence (<%> COMPLEX) ^ f is complex-valued by VALUED_0:def 7; :: thesis: verum