let x1, x2 be FinSequence of REAL ; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: ( (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 = & 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 ;
then i in dom x2 by ;
then A4: x2 /. i = x2 . i by PARTFUN1:def 6;
i in dom x1 by ;
then x1 /. i = x1 . i by PARTFUN1:def 6;
hence (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) by ; :: thesis: (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
hence (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) by ; :: thesis: verum