let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies (1_Rmatrix n) . i = Base_FinSeq (n,i) )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: (1_Rmatrix n) . i = Base_FinSeq (n,i)
then 1 <= n by XXREAL_0:2;
then A2: 1 in Seg n ;
i in Seg n by A1;
then [i,1] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:87;
then [i,1] in Indices (1. (F_Real,n)) by MATRIX_0:24;
then consider q being FinSequence of REAL such that
A3: q = (1_Rmatrix n) . i and
(1_Rmatrix n) * (i,1) = q . 1 by MATRIX_0:def 5;
len (1_Rmatrix n) = n by MATRIX_0:24;
then i in dom (1_Rmatrix n) by A1, FINSEQ_3:25;
then q in rng (1_Rmatrix n) by A3, FUNCT_1:def 3;
then A4: len q = n by MATRIX_0:def 2;
A5: for j being Nat st 1 <= j & j <= n holds
q . j = (Base_FinSeq (n,i)) . j
proof
A6: i in Seg n by A1;
let j be Nat; :: thesis: ( 1 <= j & j <= n implies q . j = (Base_FinSeq (n,i)) . j )
assume A7: ( 1 <= j & j <= n ) ; :: thesis: q . j = (Base_FinSeq (n,i)) . j
j in Seg n by A7;
then [i,j] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:87;
then A8: [i,j] in Indices (1. (F_Real,n)) by MATRIX_0:24;
then A9: ex q0 being FinSequence of REAL st
( q0 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = q0 . j ) by MATRIX_0:def 5;
per cases ( i = j or i <> j ) ;
suppose A10: i = j ; :: thesis: q . j = (Base_FinSeq (n,i)) . j
then (1. (F_Real,n)) * (i,i) = 1_ F_Real by A8, MATRIX_1:def 3;
hence q . j = (Base_FinSeq (n,i)) . j by A1, A3, A9, A10, Th75; :: thesis: verum
end;
suppose A11: i <> j ; :: thesis: q . j = (Base_FinSeq (n,i)) . j
then (1. (F_Real,n)) * (i,j) = 0. F_Real by A8, MATRIX_1:def 3;
hence q . j = (Base_FinSeq (n,i)) . j by A3, A7, A9, A11, Th76; :: thesis: verum
end;
end;
end;
len (Base_FinSeq (n,i)) = n by Th74;
hence (1_Rmatrix n) . i = Base_FinSeq (n,i) by A3, A4, A5, FINSEQ_1:14; :: thesis: verum