A2:
dom the multF of V = [: the carrier of V, the carrier of V:]
by FUNCT_2:def 1;
A3:
for z being set st z in [:V1,V1:] holds
( the multF of V || V1) . z in V1
proof
let z be
set ;
( z in [:V1,V1:] implies ( the multF of V || V1) . z in V1 )
assume A4:
z in [:V1,V1:]
;
( the multF of V || V1) . z in V1
then consider r,
x being
set such that A5:
(
r in V1 &
x in V1 )
and A6:
z = [r,x]
by ZFMISC_1:def 2;
reconsider y =
x,
r1 =
r as
Element of
V by A5;
[r,x] in dom ( the multF of V || V1)
by A2, A4, A6, RELAT_1:62, ZFMISC_1:96;
then
( the multF of V || V1) . z = r1 * y
by A6, FUNCT_1:47;
hence
( the multF of V || V1) . z in V1
by A1, A5, Def4;
verum
end;
dom ( the multF of V || V1) = [:V1,V1:]
by A2, RELAT_1:62, ZFMISC_1:96;
hence
the multF of V || V1 is BinOp of V1
by A3, FUNCT_2:3; verum