let x be set ; :: thesis: for n being Nat
for r being real number
for f1 being real-valued b₁ -long 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 number
for f1 being real-valued n -long FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let r be real number ; :: thesis: for f1 being real-valued n -long FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let f1 be real-valued n -long 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 EUCLID:3;
A2: dom ((0.REAL n) +* (x,r)) = Seg n by EUCLID:3;
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:32;
A5: dom (0.REAL n) = Seg n by EUCLID:3;

now

let z be set ; :: 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:33
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A1, A2, A3, A5, A6, A8, FUNCT_7:33 ;
:: 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:34
.= (f1 . z) * ((n |-> 0) . z)
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A9, FUNCT_7:34 ;
:: thesis: verum

end;

end;

end;

hence mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r)) by A4, A5, EUCLID:3, FUNCT_1:9; :: thesis: verum