let i be Nat; :: thesis: for n being Element of NAT st 1 <= i & i <= n holds
(1_Rmatrix n) . i = Base_FinSeq n,i
let n be Element of 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 NAT by ORDINAL1:def 13;
then i in Seg n by A1;
then [i,1] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:106;
then [i,1] in Indices (1. F_Real ,n) by MATRIX_1:25;
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_1:def 6;
len (1_Rmatrix n) = n by MATRIX_1:25;
then i in dom (1_Rmatrix n) by A1, FINSEQ_3:27;
then q in rng (1_Rmatrix n) by A3, FUNCT_1:def 5;
then A4: len q = n by MATRIX_1:def 3;
A5: for j being Nat st 1 <= j & j <= n holds
q . j = (Base_FinSeq n,i) . j

proof

i in NAT by ORDINAL1:def 13;
then 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 NAT by ORDINAL1:def 13;
then j in Seg n by A7;
then [i,j] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:106;
then A8: [i,j] in Indices (1. F_Real ,n) by MATRIX_1:25;
then A9: ex q0 being FinSequence of REAL st
( q0 = (1_Rmatrix n) . i & (1_Rmatrix n) * i,j = q0 . j ) by MATRIX_1:def 6;

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 12;
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 12;
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:18; :: thesis: verum