let n, i be Nat; :: thesis: for x being Element of REAL n st 1 <= i & i <= n holds
|(x,(Base_FinSeq n,i))| = x . i
let x be Element of REAL n; :: thesis: ( 1 <= i & i <= n implies |(x,(Base_FinSeq n,i))| = x . i )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: |(x,(Base_FinSeq n,i))| = x . i
set x2 = Base_FinSeq n,i;
A2: len (Base_FinSeq n,i) = n by MATRIXR2:74;
A3: len x = n by FINSEQ_1:def 18;
then A4: len (mlt x,(Base_FinSeq n,i)) = n by A2, MATRPROB:30;
A5: len ((x /. i) * (Base_FinSeq n,i)) = n by A2, EUCLID_2:8;
for j being Nat st 1 <= j & j <= n holds
(mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j )
assume A6: ( 1 <= j & j <= n ) ; :: thesis: (mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j
then j in Seg n by FINSEQ_1:3;
then A7: j in dom (mlt x,(Base_FinSeq n,i)) by A4, FINSEQ_1:def 3;
reconsider j0 = j as Element of NAT by ORDINAL1:def 13;

A8: now

per cases ( i = j or i <> j ) ;

case i = j ; :: thesis: ((x /. i) * (Base_FinSeq n,i)) . j = (x /. j) * ((Base_FinSeq n,i) . j)

hence ((x /. i) * (Base_FinSeq n,i)) . j = (x /. j) * ((Base_FinSeq n,i) . j) by RVSUM_1:66; :: thesis: verum

end;

case i <> j ; :: thesis: ((x /. i) * (Base_FinSeq n,i)) . j = (x /. j) * ((Base_FinSeq n,i) . j)

then A9: (Base_FinSeq n,i) . j0 = 0 by A6, MATRIXR2:76;
((x /. i) * (Base_FinSeq n,i)) . j = (x /. i) * ((Base_FinSeq n,i) . j) by RVSUM_1:66
.= (x /. j) * ((Base_FinSeq n,i) . j) by A9 ;
hence ((x /. i) * (Base_FinSeq n,i)) . j = (x /. j) * ((Base_FinSeq n,i) . j) ; :: thesis: verum

end;

end;

end;

(mlt x,(Base_FinSeq n,i)) . j = (x . j) * ((Base_FinSeq n,i) . j) by A7, RVSUM_1:86;
hence (mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j by A3, A6, A8, FINSEQ_4:24; :: thesis: verum

end;

then mlt x,(Base_FinSeq n,i) = (x /. i) * (Base_FinSeq n,i) by A4, A5, FINSEQ_1:18;
then Sum (mlt x,(Base_FinSeq n,i)) = (x /. i) * (Sum (Base_FinSeq n,i)) by RVSUM_1:117
.= (x /. i) * 1 by Th31, A1
.= x . i by A1, A3, FINSEQ_4:24 ;
hence |(x,(Base_FinSeq n,i))| = x . i ; :: thesis: verum