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 A3: dom ((<*> COMPLEX) ^ f) = Seg (0 + (len f)) by Def2;
then x >= 1 by A1, FINSEQ_1:1;
then reconsider y = x - 1 as Nat ;
y + 1 in Seg (len f) by A1, A3;
then y in Segm (len f) by NEWTON02:106;
then ((<*> COMPLEX) ^ f) . ((0 + y) + 1) = f . y by A2, Def2;
hence ((<*> COMPLEX) ^ f) . x is complex ; :: thesis: verum

end;

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