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

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

let r be Real; :: thesis: for f1 being n -element real-valued FinSequence holds |(f1,(() +* (x,r)))| = (f1 . x) * r
let f1 be n -element real-valued FinSequence; :: thesis: |(f1,(() +* (x,r)))| = (f1 . x) * r
A1: mlt (f1,(() +* (x,r))) = () +* (x,((f1 . x) * r)) by Th15;
A2: dom f1 = Seg n by FINSEQ_1:89;
A3: n in NAT by ORDINAL1:def 12;
per cases ( x in dom f1 or not x in dom f1 ) ;
suppose x in dom f1 ; :: thesis: |(f1,(() +* (x,r)))| = (f1 . x) * r
hence |(f1,(() +* (x,r)))| = (f1 . x) * r by ; :: thesis: verum
end;
suppose not x in dom f1 ; :: thesis: |(f1,(() +* (x,r)))| = (f1 . x) * r
then A4: f1 . x = 0 by FUNCT_1:def 2;
hence |(f1,(() +* (x,r)))| = Sum () by
.= (f1 . x) * r by ;
:: thesis: verum
end;
end;