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

proof

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

end;

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