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