let x be FinSequence of REAL ; :: thesis: ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) )
assume A1: len x > 0 ; :: thesis: ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
A2: ( width (LineVec2Mx x) = len x & len (LineVec2Mx x) = 1 ) by Def10;
A3: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 ) by A1, Def9;
A4: dom (ColVec2Mx x) = Seg (len (ColVec2Mx x)) by FINSEQ_1:def 3;
A5: dom (LineVec2Mx x) = Seg (len (LineVec2Mx x)) by FINSEQ_1:def 3;
A6: 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:106;
hence ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) by A2, A3, A4, A5, ZFMISC_1:106; :: thesis: verum

end;

A7: 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 A8: [j,i] in Indices (LineVec2Mx x) ; :: thesis: (ColVec2Mx x) * i,j = (LineVec2Mx x) * j,i
then j in Seg 1 by A2, A5, ZFMISC_1:106;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:3;
then A9: j = 1 by XXREAL_0:1;
i in Seg (len x) by A2, A8, ZFMISC_1:106;
then A10: i in dom x by FINSEQ_1:def 3;
A11: [i,j] in Indices (ColVec2Mx x) by A6, A8;
A12: (ColVec2Mx x) . i = <*(x . i)*> by A1, A10, Def9;
consider p being FinSequence of REAL such that
A13: ( p = (ColVec2Mx x) . i & (ColVec2Mx x) * i,j = p . j ) by A11, MATRIX_1:def 6;
thus (ColVec2Mx x) * i,j = x . i by A9, A12, A13, FINSEQ_1:57
.= (LineVec2Mx x) * j,i by A9, A10, Def10 ; :: thesis: verum

end;

hence (LineVec2Mx x) @ = ColVec2Mx x by A2, A3, A6, MATRIX_1:def 7; :: thesis: (ColVec2Mx x) @ = LineVec2Mx x
A14: for i, j being Nat holds
( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) ) by A6;
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 A6;
hence (LineVec2Mx x) * i,j = (ColVec2Mx x) * j,i by A7; :: thesis: verum

end;

hence (ColVec2Mx x) @ = LineVec2Mx x by A2, A3, A14, MATRIX_1:def 7; :: thesis: verum