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:95;
A2:
now for z being object st z in [:REAL,X1:] holds
( the Mult of X | [:REAL,X1:]) . z in X1let z be
object ;
( z in [:REAL,X1:] implies ( the Mult of X | [:REAL,X1:]) . z in X1 )assume A3:
z in [:REAL,X1:]
;
( the Mult of X | [:REAL,X1:]) . z in X1then consider r,
x being
object 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:62;
then
( the Mult of X | [:REAL,X1:]) . z = r * y
by A6, FUNCT_1:47;
hence
( the Mult of X | [:REAL,X1:]) . z in X1
by A5, Def1;
verum end;
dom ( the Mult of X | [:REAL,X1:]) = [:REAL,X1:]
by A1, RELAT_1:62;
hence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1
by A2, FUNCT_2:3; verum