now :: thesis: for x being object st x in dom <*F*> holds
<*F*> . x is complex-valued Function

let x be object ; :: thesis: ( x in dom <*F*> implies <*F*> . x is complex-valued Function )
A1: ( dom <*F*> = Seg 1 & Seg 1 = {1} ) by FINSEQ_1:2, FINSEQ_1:38;
assume x in dom <*F*> ; :: thesis: <*F*> . x is complex-valued Function
then x = 1 by A1, TARSKI:def 1;
hence <*F*> . x is complex-valued Function ; :: thesis: verum

end;

hence <*F*> is complex-functions-valued by VALUED_2:def 26; :: thesis: verum