let x be object ; :: thesis: for n being Nat
for r being Real
for f1 being b₁ -element real-valued FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let n be Nat; :: thesis: for r being Real
for f1 being n -element real-valued FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let r be Real; :: thesis: for f1 being n -element real-valued FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let f1 be n -element real-valued FinSequence; :: thesis: |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
A1: mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (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,((0.REAL n) +* (x,r)))| = (f1 . x) * r

hence |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r by A1, A2, A3, JORDAN2B:10; :: thesis: verum

end;

suppose not x in dom f1 ; :: thesis: |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r

then A4: f1 . x = 0 by FUNCT_1:def 2;
hence |(f1,((0.REAL n) +* (x,r)))| = Sum (0.REAL n) by A1, Th14
.= (f1 . x) * r by A4, A3, JORDAN2B:9 ;
:: thesis: verum

end;

end;