let x be FinSequence of REAL ; :: thesis: ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) )
A1: dom (LineVec2Mx x) = Seg (len (LineVec2Mx x)) by FINSEQ_1:def 3;
A2: width (LineVec2Mx x) = len x by Def10;
assume A3: len x > 0 ; :: thesis: ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
then A4: len (ColVec2Mx x) = len x by Def9;
A5: len (LineVec2Mx x) = 1 by Def10;
A6: width (ColVec2Mx x) = 1 by A3, Def9;
A7: dom (ColVec2Mx x) = Seg (len (ColVec2Mx x)) by FINSEQ_1:def 3;
A8: for i, j being Nat holds
( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
( [i,j] in Indices (ColVec2Mx x) iff ( i in dom (ColVec2Mx x) & j in Seg (width (ColVec2Mx x)) ) ) by ZFMISC_1:87;
hence ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) by A2, A5, A4, A6, A7, A1, ZFMISC_1:87; :: thesis: verum

end;

A9: for i, j being Nat st [j,i] in Indices (LineVec2Mx x) holds
(ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)

proof

let i, j be Nat; :: thesis: ( [j,i] in Indices (LineVec2Mx x) implies (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) )
assume A10: [j,i] in Indices (LineVec2Mx x) ; :: thesis: (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
then [i,j] in Indices (ColVec2Mx x) by A8;
then A11: ex p being FinSequence of REAL st
( p = (ColVec2Mx x) . i & (ColVec2Mx x) * (i,j) = p . j ) by MATRIX_0:def 5;
j in Seg 1 by A5, A1, A10, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A12: j = 1 by XXREAL_0:1;
i in Seg (len x) by A2, A10, ZFMISC_1:87;
then A13: i in dom x by FINSEQ_1:def 3;
then (ColVec2Mx x) . i = <*(x . i)*> by A3, Def9;
hence (ColVec2Mx x) * (i,j) = x . i by A12, A11
.= (LineVec2Mx x) * (j,i) by A12, A13, Def10 ;
:: thesis: verum

end;

hence (LineVec2Mx x) @ = ColVec2Mx x by A2, A4, A8, MATRIX_0:def 6; :: thesis: (ColVec2Mx x) @ = LineVec2Mx x
A14: for i, j being Nat st [j,i] in Indices (ColVec2Mx x) holds
(LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)

proof

let i, j be Nat; :: thesis: ( [j,i] in Indices (ColVec2Mx x) implies (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) )
assume [j,i] in Indices (ColVec2Mx x) ; :: thesis: (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
then [i,j] in Indices (LineVec2Mx x) by A8;
hence (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) by A9; :: thesis: verum

end;

for i, j being Nat holds
( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) ) by A8;
hence (ColVec2Mx x) @ = LineVec2Mx x by A5, A6, A14, MATRIX_0:def 6; :: thesis: verum