A2: dom the Mult of X = [:COMPLEX ,the carrier of X:] by FUNCT_2:def 1;
A3: [:COMPLEX ,X1:] c= [:COMPLEX ,the carrier of X:] by ZFMISC_1:118;
A4: 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 A5: z in [:COMPLEX ,X1:] ; :: thesis: (the Mult of X | [:COMPLEX ,X1:]) . z in X1
consider r, x being set such that
A6: r in COMPLEX and
A7: x in X1 and
A8: z = [r,x] by A5, ZFMISC_1:def 2;
reconsider r = r as Complex by A6;
reconsider y = x as VECTOR of X by A7;
[r,x] in dom (the Mult of X | [:COMPLEX ,X1:]) by A3, A2, A5, A8, RELAT_1:91;
then (the Mult of X | [:COMPLEX ,X1:]) . z = r * y by A8, FUNCT_1:70;
hence (the Mult of X | [:COMPLEX ,X1:]) . z in X1 by A1, A7, CLVECT_1:def 7; :: thesis: verum

end;

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