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

proof

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

per cases then ( [i,j] = [1,1] or [i,j] = [2,1] or [i,j] = [3,1] ) ;

suppose A6: [i,j] = [1,1] ; :: thesis: B * (i,j) = C * (i,j)

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

end;

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

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

end;

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

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

end;

end;

end;

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