let n be Element of NAT ; :: thesis: for x being FinSequence of REAL st len x = n & n > 0 holds
(1_Rmatrix n) * x = x
let x be FinSequence of REAL ; :: thesis: ( len x = n & n > 0 implies (1_Rmatrix n) * x = x )
assume that
A1: len x = n and
A2: n > 0 ; :: thesis: (1_Rmatrix n) * x = x
A3: len (ColVec2Mx x) = len x by A1, A2, MATRIXR1:def 9;
A4: len (Col ((ColVec2Mx x),1)) = len (ColVec2Mx x) by MATRIX_1:def 9;
A5: for k being Nat st 1 <= k & k <= len (Col ((ColVec2Mx x),1)) holds
(Col ((ColVec2Mx x),1)) . k = x . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) implies (Col ((ColVec2Mx x),1)) . k = x . k )
assume A6: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) ) ; :: thesis: (Col ((ColVec2Mx x),1)) . k = x . k
k in NAT by ORDINAL1:def 13;
then A7: k in Seg (len (ColVec2Mx x)) by A4, A6;
then A8: k in dom (ColVec2Mx x) by FINSEQ_1:def 3;
then A9: (Col ((ColVec2Mx x),1)) . k = (ColVec2Mx x) * (k,1) by MATRIX_1:def 9;
( 1 in Seg 1 & Indices (ColVec2Mx x) = [:(dom (ColVec2Mx x)),(Seg 1):] ) by A1, A2, MATRIXR1:def 9;
then [k,1] in Indices (ColVec2Mx x) by A8, ZFMISC_1:106;
then consider p being FinSequence of REAL such that
A10: p = (ColVec2Mx x) . k and
A11: (ColVec2Mx x) * (k,1) = p . 1 by MATRIX_1:def 6;
k in dom x by A3, A7, FINSEQ_1:def 3;
then p = <*(x . k)*> by A1, A2, A10, MATRIXR1:def 9;
hence (Col ((ColVec2Mx x),1)) . k = x . k by A9, A11, FINSEQ_1:57; :: thesis: verum

end;

(1_Rmatrix n) * x = Col ((MXF2MXR (MXR2MXF (ColVec2Mx x))),1) by A1, A3, Th68
.= x by A3, A4, A5, FINSEQ_1:18 ;
hence (1_Rmatrix n) * x = x ; :: thesis: verum