let D be non empty set ; :: thesis: for A being Matrix of 1,3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*>
let A be Matrix of 1,3,D; :: thesis: A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*>
reconsider B = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*> as Matrix of 1,3,D by Th24;
A1: ( len A = 1 & width A = 3 ) by MATRIX_0:23;
A2: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
A3: Indices B = [:(Seg 1),(Seg 3):] by MATRIX_0:23;
A4: Indices A = [:(Seg 1),(Seg 3):] by MATRIX_0:23;
assume A5: [i,j] in Indices A ; :: thesis: A * (i,j) = B * (i,j)
then i in {1} by A4, ZFMISC_1:87, FINSEQ_1:2;
then A6: i = 1 by TARSKI:def 1;
j in {1,2,3} by A4, A5, ZFMISC_1:87, FINSEQ_3:1;

per cases then ( [i,j] = [1,1] or [i,j] = [1,2] or [i,j] = [1,3] ) by A6, ENUMSET1:def 1;

suppose A7: [i,j] = [1,1] ; :: thesis: A * (i,j) = B * (i,j)

then consider p being FinSequence of D such that
A8: p = B . 1 and
A9: B * (1,1) = p . 1 by A3, A4, A5, MATRIX_0:def 5;
( i = 1 & j = 1 ) by A7, XTUPLE_0:1;
hence A * (i,j) = B * (i,j) by A8, A9; :: thesis: verum

end;

suppose A11: [i,j] = [1,2] ; :: thesis: A * (i,j) = B * (i,j)

then consider p being FinSequence of D such that
A12: p = B . 1 and
A13: B * (1,2) = p . 2 by A3, A4, A5, MATRIX_0:def 5;
( i = 1 & j = 2 ) by A11, XTUPLE_0:1;
hence A * (i,j) = B * (i,j) by A12, A13; :: thesis: verum

end;

suppose A15: [i,j] = [1,3] ; :: thesis: A * (i,j) = B * (i,j)

then consider p being FinSequence of D such that
A16: p = B . 1 and
A17: B * (1,3) = p . 3 by A3, A4, A5, MATRIX_0:def 5;
( i = 1 & j = 3 ) by A15, XTUPLE_0:1;
hence A * (i,j) = B * (i,j) by A16, A17; :: thesis: verum

end;

end;

end;

( len B = 1 & width B = 3 ) by MATRIX_0:23;
hence A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*> by A1, A2, MATRIX_0:21; :: thesis: verum