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:118;
A3:
for z being set st z in [:REAL ,X1:] holds
(the Mult of X | [:REAL ,X1:]) . z in X1
proof
let z be
set ;
( z in [:REAL ,X1:] implies (the Mult of X | [:REAL ,X1:]) . z in X1 )
assume A4:
z in [:REAL ,X1:]
;
(the Mult of X | [:REAL ,X1:]) . z in X1
consider r,
x being
set 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:91;
then
(the Mult of X | [:REAL ,X1:]) . z = r * y
by A7, FUNCT_1:70;
hence
(the Mult of X | [:REAL ,X1:]) . z in X1
by A1, A6, RLSUB_1:def 1;
verum
end;
dom (the Mult of X | [:REAL ,X1:]) = [:REAL ,X1:]
by A2, RELAT_1:91;
hence
the Mult of X | [:REAL ,X1:] is Function of [:REAL ,X1:],X1
by A3, FUNCT_2:5; verum