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

( 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