let x be object ; :: thesis: for n being Nat
for r being Real
for f1 being b₁ -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let n be Nat; :: thesis: for r being Real
for f1 being n -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let r be Real; :: thesis: for f1 being n -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let f1 be n -element real-valued FinSequence; :: thesis: mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
set p = (0.REAL n) +* (x,r);
A1: dom f1 = Seg n by FINSEQ_1:89;
A2: dom ((0.REAL n) +* (x,r)) = Seg n by FINSEQ_1:89;
A3: dom (mlt (f1,((0.REAL n) +* (x,r)))) = (dom f1) /\ (dom ((0.REAL n) +* (x,r))) by VALUED_1:def 4;
A4: dom ((0.REAL n) +* (x,((f1 . x) * r))) = dom (0.REAL n) by FUNCT_7:30;
A5: dom (0.REAL n) = Seg n ;

now :: thesis: for z being object st z in dom (mlt (f1,((0.REAL n) +* (x,r)))) holds
(mlt (f1,((0.REAL n) +* (x,r)))) . z = ((0.REAL n) +* (x,((f1 . x) * r))) . z

let z be object ; :: thesis: ( z in dom (mlt (f1,((0.REAL n) +* (x,r)))) implies (mlt (f1,((0.REAL n) +* (x,r)))) . b₁ = ((0.REAL n) +* (x,((f1 . x) * r))) . b₁ )
assume A6: z in dom (mlt (f1,((0.REAL n) +* (x,r)))) ; :: thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b₁ = ((0.REAL n) +* (x,((f1 . x) * r))) . b₁
A7: (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * (((0.REAL n) +* (x,r)) . z) by VALUED_1:5;

per cases ( z = x or z <> x ) ;

suppose A8: z = x ; :: thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b₁ = ((0.REAL n) +* (x,((f1 . x) * r))) . b₁

hence (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * r by A1, A2, A3, A5, A6, A7, FUNCT_7:31
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A1, A2, A3, A5, A6, A8, FUNCT_7:31 ;
:: thesis: verum

end;

suppose A9: z <> x ; :: thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b₁ = ((0.REAL n) +* (x,((f1 . x) * r))) . b₁

hence (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * ((0.REAL n) . z) by A7, FUNCT_7:32
.= (f1 . z) * ((n |-> 0) . z)
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A9, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

hence mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r)) by A4, FINSEQ_1:89; :: thesis: verum