let D be non empty set ; 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; 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;
( [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
;
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]
;
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;
A10:
B . 1
= <*(A * (1,1)),(A * (1,2)),(A * (1,3))*>
by FINSEQ_1:40;
(
i = 1 &
j = 1 )
by A7, XTUPLE_0:1;
hence
A * (
i,
j)
= B * (
i,
j)
by A10, A8, A9, FINSEQ_1:45;
verum end; suppose A11:
[i,j] = [1,2]
;
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;
A14:
B . 1
= <*(A * (1,1)),(A * (1,2)),(A * (1,3))*>
by FINSEQ_1:40;
(
i = 1 &
j = 2 )
by A11, XTUPLE_0:1;
hence
A * (
i,
j)
= B * (
i,
j)
by A14, A12, A13, FINSEQ_1:45;
verum end; suppose A15:
[i,j] = [1,3]
;
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;
A18:
B . 1
= <*(A * (1,1)),(A * (1,2)),(A * (1,3))*>
by FINSEQ_1:40;
(
i = 1 &
j = 3 )
by A15, XTUPLE_0:1;
hence
A * (
i,
j)
= B * (
i,
j)
by A18, A16, A17, FINSEQ_1:45;
verum 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; verum