let i, n 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 CARD_1:def 7;
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 12;

A9: now :: thesis: ( ( i = j & ((x /. i) * (Base_FinSeq (n,i))) . j = (x /. j) * ((Base_FinSeq (n,i)) . j) ) or ( i <> j & ((x /. i) * (Base_FinSeq (n,i))) . j = (x /. j) * ((Base_FinSeq (n,i)) . j) ) )

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:44; :: 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:44
.= (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:59;
hence (mlt (x,(Base_FinSeq (n,i)))) . j = ((x /. i) * (Base_FinSeq (n,i))) . j by A3, A7, A8, A9, FINSEQ_4:15; :: thesis: verum

end;

len ((x /. i) * (Base_FinSeq (n,i))) = n by A4, RVSUM_1:117;
then mlt (x,(Base_FinSeq (n,i))) = (x /. i) * (Base_FinSeq (n,i)) by A5, A6, FINSEQ_1:14;
then Sum (mlt (x,(Base_FinSeq (n,i)))) = (x /. i) * (Sum (Base_FinSeq (n,i))) by RVSUM_1:87
.= (x /. i) * 1 by A1, A2, Th26
.= x . i by A1, A2, A3, FINSEQ_4:15 ;
hence |(x,(Base_FinSeq (n,i)))| = x . i ; :: thesis: verum