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