A2:
( [:COMPLEX,V1:] c= [:COMPLEX, the carrier of V:] & dom the Mult of V = [:COMPLEX, the carrier of V:] )
by FUNCT_2:def 1, ZFMISC_1:95;
A3:
for z being object st z in [:COMPLEX,V1:] holds
( the Mult of V | [:COMPLEX,V1:]) . z in V1
proof
let z be
object ;
( z in [:COMPLEX,V1:] implies ( the Mult of V | [:COMPLEX,V1:]) . z in V1 )
assume A4:
z in [:COMPLEX,V1:]
;
( the Mult of V | [:COMPLEX,V1:]) . z in V1
consider r,
x being
object such that A5:
r in COMPLEX
and A6:
x in V1
and A7:
z = [r,x]
by A4, ZFMISC_1:def 2;
reconsider r =
r as
Complex by A5;
reconsider y =
x as
VECTOR of
V by A6;
[r,x] in dom ( the Mult of V | [:COMPLEX,V1:])
by A2, A4, A7, RELAT_1:62;
then
( the Mult of V | [:COMPLEX,V1:]) . z = r * y
by A7, FUNCT_1:47;
hence
( the Mult of V | [:COMPLEX,V1:]) . z in V1
by A1, A6;
verum
end;
dom ( the Mult of V | [:COMPLEX,V1:]) = [:COMPLEX,V1:]
by A2, RELAT_1:62;
hence
the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1
by A3, FUNCT_2:3; verum