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