let D be non empty set ; :: thesis:
let A be Matrix of 3,D; :: thesis:
reconsider B = <*<*(A * 1,1),(A * 1,2),(A * 1,3)*>,<*(A * 2,1),(A * 2,2),(A * 2,3)*>,<*(A * 3,1),(A * 3,2),(A * 3,3)*>*> as Matrix of 3,D by Th35;
A1: ( len B = 3 & width B = 3 ) by MATRIX_1:25;
A2: ( len A = 3 & width A = 3 ) by MATRIX_1:25;
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:
assume A3: [i,j] in Indices A ; :: thesis:
A4: Indices B = [:(Seg 3),(Seg 3):] by MATRIX_1:25;
A5: Indices A = [:(Seg 3),(Seg 3):] by MATRIX_1:25;
then A6: ( i in Seg 3 & j in Seg 3 ) by A3, ZFMISC_1:106;
A7: ( i in {1,2,3} & j in {1,2,3} ) by A3, A5, FINSEQ_3:1, ZFMISC_1:106;
A8: 1 in Seg 3 ;
A9: 2 in Seg 3 ;
A10: 3 in Seg 3 ;
A11: [i,1] in Indices A by A5, A6, A8, ZFMISC_1:106;
A12: [i,2] in Indices A by A5, A6, A9, ZFMISC_1:106;
A13: [i,3] in Indices A by A5, A6, A10, ZFMISC_1:106;

now

per cases by A7, ENUMSET1:def 1;

case A14: i = 1 ; :: thesis:

reconsider p0 = <*(A * 1,1),(A * 1,2),(A * 1,3)*> as FinSequence of D ;
A15: ( len p0 = 3 & p0 . 1 = A * 1,1 & p0 . 2 = A * 1,2 & p0 . 3 = A * 1,3 ) by FINSEQ_1:62;
consider p2 being FinSequence of D such that
A16: ( p2 = A . i & A * i,1 = p2 . 1 ) by A11, MATRIX_1:def 6;
consider p22 being FinSequence of D such that
A17: ( p22 = A . i & A * i,2 = p22 . 2 ) by A12, MATRIX_1:def 6;
consider p23 being FinSequence of D such that
A18: ( p23 = A . i & A * i,3 = p23 . 3 ) by A13, MATRIX_1:def 6;
A19: len p2 = 3 by A6, A16, Th36;
for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k

proof

let k be Nat; :: thesis:
A20: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= len p0 ) ; :: thesis:
then A21: k in Seg 3 by A15, A20;

per cases by A21, ENUMSET1:def 1, FINSEQ_3:1;

suppose k = 1 ; :: thesis:

hence p0 . k = p2 . k by A14, A16, FINSEQ_1:62; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence p0 . k = p2 . k by A14, A16, A17, FINSEQ_1:62; :: thesis:

end;

suppose k = 3 ; :: thesis:

hence p0 . k = p2 . k by A14, A16, A18, FINSEQ_1:62; :: thesis:

end;

then A22: p0 = A . i by A15, A16, A19, FINSEQ_1:18;
consider p being FinSequence of D such that
A23: ( p = B . i & B * i,j = p . j ) by A3, A4, A5, MATRIX_1:def 6;
B * i,j = p0 . j by A14, A23, FINSEQ_1:62;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A22; :: thesis:

end;

case A24: i = 2 ; :: thesis:

reconsider p0 = <*(A * 2,1),(A * 2,2),(A * 2,3)*> as FinSequence of D ;
A25: ( len p0 = 3 & p0 . 1 = A * 2,1 & p0 . 2 = A * 2,2 & p0 . 3 = A * 2,3 ) by FINSEQ_1:62;
consider p2 being FinSequence of D such that
A26: ( p2 = A . i & A * i,1 = p2 . 1 ) by A11, MATRIX_1:def 6;
consider p22 being FinSequence of D such that
A27: ( p22 = A . i & A * i,2 = p22 . 2 ) by A12, MATRIX_1:def 6;
consider p23 being FinSequence of D such that
A28: ( p23 = A . i & A * i,3 = p23 . 3 ) by A13, MATRIX_1:def 6;
A29: len p2 = 3 by A6, A26, Th36;
for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k

proof

let k be Nat; :: thesis:
A30: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= len p0 ) ; :: thesis:
then A31: k in {1,2,3} by A25, A30, FINSEQ_3:1;

per cases by A31, ENUMSET1:def 1;

suppose k = 1 ; :: thesis:

hence p0 . k = p2 . k by A24, A26, FINSEQ_1:62; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence p0 . k = p2 . k by A24, A26, A27, FINSEQ_1:62; :: thesis:

end;

suppose k = 3 ; :: thesis:

hence p0 . k = p2 . k by A24, A26, A28, FINSEQ_1:62; :: thesis:

end;

then A32: p0 = A . i by A25, A26, A29, FINSEQ_1:18;
consider p being FinSequence of D such that
A33: ( p = B . i & B * i,j = p . j ) by A3, A4, A5, MATRIX_1:def 6;
B * i,j = p0 . j by A24, A33, FINSEQ_1:62;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A32; :: thesis:

end;

case A34: i = 3 ; :: thesis:

reconsider p0 = <*(A * 3,1),(A * 3,2),(A * 3,3)*> as FinSequence of D ;
A35: ( len p0 = 3 & p0 . 1 = A * 3,1 & p0 . 2 = A * 3,2 & p0 . 3 = A * 3,3 ) by FINSEQ_1:62;
consider p2 being FinSequence of D such that
A36: ( p2 = A . i & A * i,1 = p2 . 1 ) by A11, MATRIX_1:def 6;
consider p22 being FinSequence of D such that
A37: ( p22 = A . i & A * i,2 = p22 . 2 ) by A12, MATRIX_1:def 6;
consider p23 being FinSequence of D such that
A38: ( p23 = A . i & A * i,3 = p23 . 3 ) by A13, MATRIX_1:def 6;
A39: len p2 = 3 by A6, A36, Th36;
for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k

proof

let k be Nat; :: thesis:
A40: k in NAT by ORDINAL1:def 13;
assume ( 1 <= k & k <= len p0 ) ; :: thesis:
then A41: k in {1,2,3} by A35, A40, FINSEQ_3:1;

per cases by A41, ENUMSET1:def 1;

suppose k = 1 ; :: thesis:

hence p0 . k = p2 . k by A34, A36, FINSEQ_1:62; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence p0 . k = p2 . k by A34, A36, A37, FINSEQ_1:62; :: thesis:

end;

suppose k = 3 ; :: thesis:

hence p0 . k = p2 . k by A34, A36, A38, FINSEQ_1:62; :: thesis:

end;

then A42: p0 = A . i by A35, A36, A39, FINSEQ_1:18;
consider p being FinSequence of D such that
A43: ( p = B . i & B * i,j = p . j ) by A3, A4, A5, MATRIX_1:def 6;
B * i,j = p0 . j by A34, A43, FINSEQ_1:62;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A42; :: thesis:

end;

hence A * i,j = B * i,j by A3, MATRIX_1:def 6; :: thesis:

end;

hence A = <*<*(A * 1,1),(A * 1,2),(A * 1,3)*>,<*(A * 2,1),(A * 2,2),(A * 2,3)*>,<*(A * 3,1),(A * 3,2),(A * 3,3)*>*> by A1, A2, MATRIX_1:21; :: thesis: