let D be non empty set ; :: thesis: for A being Matrix of 3,D holds 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)*>*>
let A be Matrix of 3,D; :: thesis: 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)*>*>
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 A = 3 & width A = 3 ) by MATRIX_1:25;
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 3),(Seg 3):] by MATRIX_1:25;
A4: Indices A = [:(Seg 3),(Seg 3):] by MATRIX_1:25;
assume A5: [i,j] in Indices A ; :: thesis: A * i,j = B * i,j
then A6: i in Seg 3 by A4, ZFMISC_1:106;
2 in Seg 3 ;
then A7: [i,2] in Indices A by A4, A6, ZFMISC_1:106;
1 in Seg 3 ;
then A8: [i,1] in Indices A by A4, A6, ZFMISC_1:106;
3 in Seg 3 ;
then A9: [i,3] in Indices A by A4, A6, ZFMISC_1:106;
A10: i in {1,2,3} by A5, A4, FINSEQ_3:1, ZFMISC_1:106;
now
per cases ( i = 1 or i = 2 or i = 3 ) by A10, ENUMSET1:def 1;
case A11: i = 1 ; :: thesis: ex p being FinSequence of D st
( p = A . i & B * i,j = p . j )
reconsider p0 = <*(A * 1,1),(A * 1,2),(A * 1,3)*> as FinSequence of D ;
A12: len p0 = 3 by FINSEQ_1:62;
A13: ex p23 being FinSequence of D st
( p23 = A . i & A * i,3 = p23 . 3 ) by A9, MATRIX_1:def 6;
consider p2 being FinSequence of D such that
A14: p2 = A . i and
A15: A * i,1 = p2 . 1 by A8, MATRIX_1:def 6;
A16: ex p22 being FinSequence of D st
( p22 = A . i & A * i,2 = p22 . 2 ) by A7, MATRIX_1:def 6;
A17: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A18: ( 1 <= k & k <= len p0 ) ; :: thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def 13;
then A19: k in Seg 3 by A12, A18;
per cases ( k = 1 or k = 2 or k = 3 ) by A19, ENUMSET1:def 1, FINSEQ_3:1;
suppose k = 1 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A15, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A16, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A13, FINSEQ_1:62; :: thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * i,j = p . j ) by A5, A3, A4, MATRIX_1:def 6;
then A20: B * i,j = p0 . j by A11, FINSEQ_1:62;
len p2 = 3 by A6, A14, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A12, A14, A17, A20, FINSEQ_1:18; :: thesis: verum
end;
case A21: i = 2 ; :: thesis: ex p being FinSequence of D st
( p = A . i & B * i,j = p . j )
reconsider p0 = <*(A * 2,1),(A * 2,2),(A * 2,3)*> as FinSequence of D ;
A22: len p0 = 3 by FINSEQ_1:62;
A23: ex p23 being FinSequence of D st
( p23 = A . i & A * i,3 = p23 . 3 ) by A9, MATRIX_1:def 6;
consider p2 being FinSequence of D such that
A24: p2 = A . i and
A25: A * i,1 = p2 . 1 by A8, MATRIX_1:def 6;
A26: ex p22 being FinSequence of D st
( p22 = A . i & A * i,2 = p22 . 2 ) by A7, MATRIX_1:def 6;
A27: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A28: ( 1 <= k & k <= len p0 ) ; :: thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def 13;
then A29: k in {1,2,3} by A22, A28, FINSEQ_3:1;
per cases ( k = 1 or k = 2 or k = 3 ) by A29, ENUMSET1:def 1;
suppose k = 1 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A25, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A26, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A23, FINSEQ_1:62; :: thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * i,j = p . j ) by A5, A3, A4, MATRIX_1:def 6;
then A30: B * i,j = p0 . j by A21, FINSEQ_1:62;
len p2 = 3 by A6, A24, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A22, A24, A27, A30, FINSEQ_1:18; :: thesis: verum
end;
case A31: i = 3 ; :: thesis: ex p being FinSequence of D st
( p = A . i & B * i,j = p . j )
reconsider p0 = <*(A * 3,1),(A * 3,2),(A * 3,3)*> as FinSequence of D ;
A32: len p0 = 3 by FINSEQ_1:62;
A33: ex p23 being FinSequence of D st
( p23 = A . i & A * i,3 = p23 . 3 ) by A9, MATRIX_1:def 6;
consider p2 being FinSequence of D such that
A34: p2 = A . i and
A35: A * i,1 = p2 . 1 by A8, MATRIX_1:def 6;
A36: ex p22 being FinSequence of D st
( p22 = A . i & A * i,2 = p22 . 2 ) by A7, MATRIX_1:def 6;
A37: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A38: ( 1 <= k & k <= len p0 ) ; :: thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def 13;
then A39: k in {1,2,3} by A32, A38, FINSEQ_3:1;
per cases ( k = 1 or k = 2 or k = 3 ) by A39, ENUMSET1:def 1;
suppose k = 1 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A35, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A36, FINSEQ_1:62; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A33, FINSEQ_1:62; :: thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * i,j = p . j ) by A5, A3, A4, MATRIX_1:def 6;
then A40: B * i,j = p0 . j by A31, FINSEQ_1:62;
len p2 = 3 by A6, A34, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * i,j = p . j ) by A32, A34, A37, A40, FINSEQ_1:18; :: thesis: verum
end;
end;
end;
hence A * i,j = B * i,j by A5, MATRIX_1:def 6; :: thesis: verum
end;
( len B = 3 & width B = 3 ) by MATRIX_1:25;
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: verum