let x be object ; for n being Nat
for r being Real
for f1 being b1 -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let n be Nat; for r being Real
for f1 being n -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let r be Real; for f1 being n -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let f1 be n -element real-valued FinSequence; 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 FINSEQ_1:89;
A2:
dom ((0.REAL n) +* (x,r)) = Seg n
by FINSEQ_1:89;
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:30;
A5:
dom (0.REAL n) = Seg n
;
now for z being object st z in dom (mlt (f1,((0.REAL n) +* (x,r)))) holds
(mlt (f1,((0.REAL n) +* (x,r)))) . z = ((0.REAL n) +* (x,((f1 . x) * r))) . zlet z be
object ;
( z in dom (mlt (f1,((0.REAL n) +* (x,r)))) implies (mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1 )assume A6:
z in dom (mlt (f1,((0.REAL n) +* (x,r))))
;
(mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1A7:
(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
;
(mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1hence (mlt (f1,((0.REAL n) +* (x,r)))) . z =
(f1 . z) * r
by A1, A2, A3, A5, A6, A7, FUNCT_7:31
.=
((0.REAL n) +* (x,((f1 . x) * r))) . z
by A1, A2, A3, A5, A6, A8, FUNCT_7:31
;
verum end; end; end;
hence
mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
by A4, FINSEQ_1:89; verum