let x be XFinSequence of REAL ; :: thesis: for y being Real_Sequence holds
( x (#) y is finite Sequence of REAL & dom (x (#) y) = dom x & ( for i being object st i in dom x holds
(x (#) y) . i = (x . i) * (y . i) ) )
let y be Real_Sequence; :: thesis: ( x (#) y is finite Sequence of REAL & dom (x (#) y) = dom x & ( for i being object st i in dom x holds
(x (#) y) . i = (x . i) * (y . i) ) )
P1: dom y = NAT by FUNCT_2:def 1;
P2: dom (x (#) y) = (dom x) /\ (dom y) by VALUED_1:def 4
.= dom x by XBOOLE_1:28, P1 ;
then x (#) y is Sequence of rng (x (#) y) by ORDINAL1:31;
hence ( x (#) y is finite Sequence of REAL & dom (x (#) y) = dom x & ( for i being object st i in dom x holds
(x (#) y) . i = (x . i) * (y . i) ) ) by P2, VALUED_1:def 4, ORDINAL1:32; :: thesis: verum