let x1, x2 be FinSequence of REAL ; for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
let i be Element of NAT ; ( i in dom (mlt (x1,x2)) implies ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) )
assume A1:
i in dom (mlt (x1,x2))
; ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
A2:
mlt (x1,x2) = multreal .: (x1,x2)
by RVSUM_1:def 9;
( dom multreal = [:REAL,REAL:] & rng x1 c= REAL )
by FUNCT_2:def 1;
then
[:(rng x1),(rng x2):] c= dom multreal
by ZFMISC_1:96;
then A3:
dom (mlt (x1,x2)) = (dom x1) /\ (dom x2)
by A2, FUNCOP_1:69;
then
i in dom x2
by A1, XBOOLE_0:def 4;
then A4:
x2 /. i = x2 . i
by PARTFUN1:def 6;
i in dom x1
by A1, A3, XBOOLE_0:def 4;
then
x1 /. i = x1 . i
by PARTFUN1:def 6;
hence
(mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i)
by A4, RVSUM_1:59; (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
hence
(mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
by A1, PARTFUN1:def 6; verum