A2:
( [: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;

A3: for z being object st z in [:REAL,X1:] holds

( the Mult of X | [:REAL,X1:]) . z in X1

hence the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1 by A3, FUNCT_2:3; :: thesis: verum

A3: for z being object st z in [:REAL,X1:] holds

( the Mult of X | [:REAL,X1:]) . z in X1

proof

dom ( the Mult of X | [:REAL,X1:]) = [:REAL,X1:]
by A2, RELAT_1:62;
let z be object ; :: thesis: ( z in [:REAL,X1:] implies ( the Mult of X | [:REAL,X1:]) . z in X1 )

assume A4: z in [:REAL,X1:] ; :: thesis: ( the Mult of X | [:REAL,X1:]) . z in X1

consider r, x being object such that

A5: r in REAL and

A6: x in X1 and

A7: z = [r,x] by A4, ZFMISC_1:def 2;

reconsider r = r as Real by A5;

reconsider y = x as VECTOR of X by A6;

[r,x] in dom ( the Mult of X | [:REAL,X1:]) by A2, A4, A7, RELAT_1:62;

then ( the Mult of X | [:REAL,X1:]) . z = r * y by A7, FUNCT_1:47;

hence ( the Mult of X | [:REAL,X1:]) . z in X1 by A1, A6; :: thesis: verum

end;assume A4: z in [:REAL,X1:] ; :: thesis: ( the Mult of X | [:REAL,X1:]) . z in X1

consider r, x being object such that

A5: r in REAL and

A6: x in X1 and

A7: z = [r,x] by A4, ZFMISC_1:def 2;

reconsider r = r as Real by A5;

reconsider y = x as VECTOR of X by A6;

[r,x] in dom ( the Mult of X | [:REAL,X1:]) by A2, A4, A7, RELAT_1:62;

then ( the Mult of X | [:REAL,X1:]) . z = r * y by A7, FUNCT_1:47;

hence ( the Mult of X | [:REAL,X1:]) . z in X1 by A1, A6; :: thesis: verum

hence the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1 by A3, FUNCT_2:3; :: thesis: verum