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