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 A1: ( len x = n & n > 0 ) ; :: thesis: (1_Rmatrix n) * x = x
then A2: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 ) by MATRIXR1:def 9;
A3: ( len (Col (ColVec2Mx x),1) = len (ColVec2Mx x) & ( for j2 being Nat st j2 in dom (ColVec2Mx x) holds
(Col (ColVec2Mx x),1) . j2 = (ColVec2Mx x) * j2,1 ) ) by MATRIX_1:def 9;
A4: 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 )
A5: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= len (Col (ColVec2Mx x),1) ) ; :: thesis: (Col (ColVec2Mx x),1) . k = x . k
then A6: k in Seg (len (ColVec2Mx x)) by A3, A5;
then A7: k in dom (ColVec2Mx x) by FINSEQ_1:def 3;
then A8: (Col (ColVec2Mx x),1) . k = (ColVec2Mx x) * k,1 by MATRIX_1:def 9;
A9: 1 in Seg 1 ;
A10: k in dom x by A2, A6, FINSEQ_1:def 3;
Indices (ColVec2Mx x) = [:(dom (ColVec2Mx x)),(Seg 1):] by A1, MATRIXR1:def 9;
then [k,1] in Indices (ColVec2Mx x) by A7, A9, ZFMISC_1:106;
then consider p being FinSequence of REAL such that
A11: ( p = (ColVec2Mx x) . k & (ColVec2Mx x) * k,1 = p . 1 ) by MATRIX_1:def 6;
p = <*(x . k)*> by A1, A10, A11, MATRIXR1:def 9;
hence (Col (ColVec2Mx x),1) . k = x . k by A8, A11, FINSEQ_1:57; :: thesis: verum

end;

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