let x be set ; :: thesis: for n being Nat
for r being real number
for f1 being real-valued b₁ -long FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let n be Nat; :: thesis: for r being real number
for f1 being real-valued n -long FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let r be real number ; :: thesis: for f1 being real-valued n -long FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let f1 be real-valued n -long 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 EUCLID:3;
A3: n in NAT by ORDINAL1:def 13;
A4: (f1 . x) * r in REAL by XREAL_0:def 1;

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, A4, JORDAN2B:14; :: thesis: verum

end;

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

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

end;

end;