let x be object ; :: thesis: for n being Nat
for r being Real
for f1 being b1 -element real-valued FinSequence holds mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r))

let n be Nat; :: thesis: for r being Real
for f1 being n -element real-valued FinSequence holds mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r))

let r be Real; :: thesis: for f1 being n -element real-valued FinSequence holds mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r))
let f1 be n -element real-valued FinSequence; :: thesis: mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r))
set p = () +* (x,r);
A1: dom f1 = Seg n by FINSEQ_1:89;
A2: dom (() +* (x,r)) = Seg n by FINSEQ_1:89;
A3: dom (mlt (f1,(() +* (x,r)))) = (dom f1) /\ (dom (() +* (x,r))) by VALUED_1:def 4;
A4: dom (() +* (x,((f1 . x) * r))) = dom () by FUNCT_7:30;
A5: dom () = Seg n ;
now :: thesis: for z being object st z in dom (mlt (f1,(() +* (x,r)))) holds
(mlt (f1,(() +* (x,r)))) . z = (() +* (x,((f1 . x) * r))) . z
let z be object ; :: thesis: ( z in dom (mlt (f1,(() +* (x,r)))) implies (mlt (f1,(() +* (x,r)))) . b1 = (() +* (x,((f1 . x) * r))) . b1 )
assume A6: z in dom (mlt (f1,(() +* (x,r)))) ; :: thesis: (mlt (f1,(() +* (x,r)))) . b1 = (() +* (x,((f1 . x) * r))) . b1
A7: (mlt (f1,(() +* (x,r)))) . z = (f1 . z) * ((() +* (x,r)) . z) by VALUED_1:5;
per cases ( z = x or z <> x ) ;
suppose A8: z = x ; :: thesis: (mlt (f1,(() +* (x,r)))) . b1 = (() +* (x,((f1 . x) * r))) . b1
hence (mlt (f1,(() +* (x,r)))) . z = (f1 . z) * r by A1, A2, A3, A5, A6, A7, FUNCT_7:31
.= (() +* (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,(() +* (x,r)))) . b1 = (() +* (x,((f1 . x) * r))) . b1
hence (mlt (f1,(() +* (x,r)))) . z = (f1 . z) * (() . z) by
.= (f1 . z) * ((n |-> 0) . z)
.= (() +* (x,((f1 . x) * r))) . z by ;
:: thesis: verum
end;
end;
end;
hence mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r)) by ; :: thesis: verum