let n be Nat; :: thesis: for x being FinSequence of REAL st len x = n holds
x * (1_Rmatrix n) = x
let x be FinSequence of REAL ; :: thesis: ( len x = n implies x * (1_Rmatrix n) = x )
A1: width (LineVec2Mx x) = len x by MATRIXR1:def 10;
assume len x = n ; :: thesis: x * (1_Rmatrix n) = x
then x * (1_Rmatrix n) = Line ((MXF2MXR (MXR2MXF (LineVec2Mx x))),1) by A1, Th67
.= x by MATRIXR1:48 ;
hence x * (1_Rmatrix n) = x ; :: thesis: verum