A1: ( [:COMPLEX,V1:] c= [:COMPLEX, the carrier of V:] & dom the Mult of V = [:COMPLEX, the carrier of V:] ) by FUNCT_2:def 1, ZFMISC_1:95;
A2: for z being set st z in [:COMPLEX,V1:] holds
( the Mult of V | [:COMPLEX,V1:]) . z in V1

proof

let z be set ; :: thesis: ( z in [:COMPLEX,V1:] implies ( the Mult of V | [:COMPLEX,V1:]) . z in V1 )
assume A3: z in [:COMPLEX,V1:] ; :: thesis: ( the Mult of V | [:COMPLEX,V1:]) . z in V1
consider r, x being set such that
A4: r in COMPLEX and
A5: x in V1 and
A6: z = [r,x] by A3, ZFMISC_1:def 2;
reconsider r = r as Complex by A4;
reconsider y = x as VECTOR of V by A5;
[r,x] in dom ( the Mult of V | [:COMPLEX,V1:]) by A1, A3, A6, RELAT_1:62;
then ( the Mult of V | [:COMPLEX,V1:]) . z = r * y by A6, FUNCT_1:47;
hence ( the Mult of V | [:COMPLEX,V1:]) . z in V1 by B1, A5, Def2; :: thesis: verum

end;

dom ( the Mult of V | [:COMPLEX,V1:]) = [:COMPLEX,V1:] by A1, RELAT_1:62;
hence the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1 by A2, FUNCT_2:3; :: thesis: verum