let K be Field; :: thesis: for i, n being Nat st 1 <= i & i <= n holds
(1. K,n) . i = Base_FinSeq K,n,i
let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies (1. K,n) . i = Base_FinSeq K,n,i )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: (1. K,n) . i = Base_FinSeq K,n,i
then 1 <= n by XXREAL_0:2;
then [i,1] in Indices (1. K,n) by A1, MATRIX_1:38;
then consider q being FinSequence of K such that
A2: q = (1. K,n) . i and
(1. K,n) * i,1 = q . 1 by MATRIX_1:def 6;
len (1. K,n) = n by MATRIX_1:25;
then i in dom (1. K,n) by A1, FINSEQ_3:27;
then q in rng (1. K,n) by A2, FUNCT_1:def 5;
then A3: len q = n by MATRIX_1:def 3;
A4: for j being Nat st 1 <= j & j <= n holds
q . j = (Base_FinSeq K,n,i) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= n implies q . j = (Base_FinSeq K,n,i) . j )
assume A5: ( 1 <= j & j <= n ) ; :: thesis: q . j = (Base_FinSeq K,n,i) . j
then A6: [i,j] in Indices (1. K,n) by A1, MATRIX_1:38;
then A7: ex q0 being FinSequence of K st
( q0 = (1. K,n) . i & (1. K,n) * i,j = q0 . j ) by MATRIX_1:def 6;

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

suppose A8: i = j ; :: thesis: q . j = (Base_FinSeq K,n,i) . j

then (1. K,n) * i,i = 1_ K by A6, MATRIX_1:def 12;
hence q . j = (Base_FinSeq K,n,i) . j by A1, A2, A7, A8, Th24; :: thesis: verum

end;

suppose A9: i <> j ; :: thesis: q . j = (Base_FinSeq K,n,i) . j

then q . j = 0. K by A2, A6, A7, MATRIX_1:def 12;
hence q . j = (Base_FinSeq K,n,i) . j by A5, A9, Th25; :: thesis: verum

end;

end;

end;

len (Base_FinSeq K,n,i) = n by Th23;
hence (1. K,n) . i = Base_FinSeq K,n,i by A2, A3, A4, FINSEQ_1:18; :: thesis: verum