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_0:31;
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_0:def 5;
len (1. (K,n)) = n by MATRIX_0:24;
then i in dom (1. (K,n)) by A1, FINSEQ_3:25;
then q in rng (1. (K,n)) by A2, FUNCT_1:def 3;
then A3: len q = n by MATRIX_0:def 2;
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_0:31;
then A7: ex q0 being FinSequence of K st
( q0 = (1. (K,n)) . i & (1. (K,n)) * (i,j) = q0 . j ) by MATRIX_0:def 5;
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 3;
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 3;
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:14; :: thesis: verum