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_0:24;
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_0:24;
A4: Indices A = [:(Seg 3),(Seg 3):] by MATRIX_0:24;
assume A5: [i,j] in Indices A ; :: thesis: A * (i,j) = B * (i,j)
then A6: i in Seg 3 by A4, ZFMISC_1:87;
2 in Seg 3 ;
then A7: [i,2] in Indices A by A4, A6, ZFMISC_1:87;
1 in Seg 3 ;
then A8: [i,1] in Indices A by A4, A6, ZFMISC_1:87;
3 in Seg 3 ;
then A9: [i,3] in Indices A by A4, A6, ZFMISC_1:87;
A10: i in {1,2,3} by A5, A4, FINSEQ_3:1, ZFMISC_1:87;
now :: thesis: ( ( i = 1 & ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) ) or ( i = 2 & ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) ) or ( i = 3 & ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) ) )
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:45;
A13: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A14: p2 = A . i and
A15: A * (i,1) = p2 . 1 by A8, MATRIX_0:def 5;
A16: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_0:def 5;
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
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; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A16; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A13; :: 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_0:def 5;
then A20: B * (i,j) = p0 . j by A11;
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:14; :: 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:45;
A23: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A24: p2 = A . i and
A25: A * (i,1) = p2 . 1 by A8, MATRIX_0:def 5;
A26: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_0:def 5;
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
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; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A26; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A23; :: 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_0:def 5;
then A30: B * (i,j) = p0 . j by A21;
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:14; :: 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:45;
A33: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A34: p2 = A . i and
A35: A * (i,1) = p2 . 1 by A8, MATRIX_0:def 5;
A36: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_0:def 5;
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
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; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A36; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A33; :: 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_0:def 5;
then A40: B * (i,j) = p0 . j by A31;
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:14; :: thesis: verum
end;
end;
end;
hence A * (i,j) = B * (i,j) by A5, MATRIX_0:def 5; :: thesis: verum
end;
( len B = 3 & width B = 3 ) by MATRIX_0:24;
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_0:21; :: thesis: verum