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 that
A1: 1 <= i and
A2: i <= n ; :: thesis: |(x,(Base_FinSeq n,i))| = x . i
set x2 = Base_FinSeq n,i;
A3: len x = n by FINSEQ_1:def 18;
A4: len (Base_FinSeq n,i) = n by MATRIXR2:74;
then A5: len (mlt x,(Base_FinSeq n,i)) = n by A3, MATRPROB:30;
A6: 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 that
A7: 1 <= j and
A8: j <= n ; :: thesis: (mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j
reconsider j0 = j as Element of NAT by ORDINAL1:def 13;

A9: 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 A10: (Base_FinSeq n,i) . j0 = 0 by A7, A8, 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 A10 ;
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 RVSUM_1:86;
hence (mlt x,(Base_FinSeq n,i)) . j = ((x /. i) * (Base_FinSeq n,i)) . j by A3, A7, A8, A9, FINSEQ_4:24; :: thesis: verum

end;

len ((x /. i) * (Base_FinSeq n,i)) = n by A4, RVSUM_1:147;
then mlt x,(Base_FinSeq n,i) = (x /. i) * (Base_FinSeq n,i) by A5, A6, 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 A1, A2, Th29
.= x . i by A1, A2, A3, FINSEQ_4:24 ;
hence |(x,(Base_FinSeq n,i))| = x . i ; :: thesis: verum