A1: ( [:REAL ,X1:] c= [:REAL ,the carrier of X:] & dom the Mult of X = [:REAL ,the carrier of X:] ) by FUNCT_2:def 1, ZFMISC_1:118;

A2: now

let z be set ; :: thesis: ( z in [:REAL ,X1:] implies (the Mult of X | [:REAL ,X1:]) . z in X1 )
assume A3: z in [:REAL ,X1:] ; :: thesis: (the Mult of X | [:REAL ,X1:]) . z in X1
then consider r, x being set such that
A4: r in REAL and
A5: x in X1 and
A6: z = [r,x] by ZFMISC_1:def 2;
reconsider r = r as Real by A4;
reconsider y = x as VECTOR of X by A5;
[r,x] in dom (the Mult of X | [:REAL ,X1:]) by A1, A3, A6, RELAT_1:91;
then (the Mult of X | [:REAL ,X1:]) . z = r * y by A6, FUNCT_1:70;
hence (the Mult of X | [:REAL ,X1:]) . z in X1 by A5, Def1; :: thesis: verum

end;

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