let D, E be non empty set ; for M being Matrix of D
for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) holds
M = L
let M be Matrix of D; for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) holds
M = L
let L be Matrix of E; ( len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) implies M = L )
assume that
A1:
len M = len L
and
A2:
width M = width L
and
A3:
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j)
; M = L
M is Matrix of E
proof
consider n being
Nat such that A0:
for
x being
object st
x in rng M holds
ex
p being
FinSequence of
D st
(
x = p &
len p = n )
by MATRIX_0:9;
per cases
( len M = 0 or len M <> 0 )
;
suppose I0:
len M <> 0
;
M is Matrix of E
for
x being
object st
x in rng M holds
ex
p being
FinSequence of
E st
(
x = p &
len p = n )
proof
let x be
object ;
( x in rng M implies ex p being FinSequence of E st
( x = p & len p = n ) )
assume S1:
x in rng M
;
ex p being FinSequence of E st
( x = p & len p = n )
then consider p being
FinSequence of
D such that S3:
(
x = p &
len p = n )
by A0;
X1:
width M = n
by S1, S3, MATRIX_0:def 3, I0;
for
z being
object st
z in rng p holds
z in E
proof
let z be
object ;
( z in rng p implies z in E )
assume
z in rng p
;
z in E
then consider j1 being
object such that S4:
(
j1 in dom p &
z = p . j1 )
by FUNCT_1:def 3;
S5:
j1 in Seg n
by S3, S4, FINSEQ_1:def 3;
reconsider j1 =
j1 as
Nat by S4;
consider i1 being
object such that S6:
(
i1 in dom M &
x = M . i1 )
by S1, FUNCT_1:def 3;
reconsider i1 =
i1 as
Nat by S6;
S8:
[i1,j1] in Indices M
by S6, S5, X1, ZFMISC_1:87;
then consider q being
FinSequence of
D such that S9:
(
q = M . i1 &
M * (
i1,
j1)
= q . j1 )
by MATRIX_0:def 5;
M * (
i1,
j1)
= L * (
i1,
j1)
by A3, S8;
hence
z in E
by S3, S4, S6, S9;
verum
end;
then
rng p c= E
;
then reconsider p =
p as
FinSequence of
E by FINSEQ_1:def 4;
take
p
;
( x = p & len p = n )
thus
(
x = p &
len p = n )
by S3;
verum
end; hence
M is
Matrix of
E
by MATRIX_0:9;
verum end; end;
end;
then reconsider L0 = M as Matrix of E ;
for i, j being Nat st [i,j] in Indices L0 holds
L0 * (i,j) = L * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices L0 implies L0 * (i,j) = L * (i,j) )
assume X3:
[i,j] in Indices L0
;
L0 * (i,j) = L * (i,j)
then consider q being
FinSequence of
D such that S9:
(
q = M . i &
M * (
i,
j)
= q . j )
by MATRIX_0:def 5;
consider p being
FinSequence of
E such that T9:
(
p = L0 . i &
L0 * (
i,
j)
= p . j )
by MATRIX_0:def 5, X3;
thus
L0 * (
i,
j)
= L * (
i,
j)
by A3, S9, T9, X3;
verum
end;
hence
M = L
by A1, A2, MATRIX_0:21; verum