let D be non empty set ; for M1, M2 being Matrix of D st len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
let M1, M2 be Matrix of D; ( len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) implies M1 = M2 )
assume that
A1:
len M1 = len M2
and
A2:
width M1 = width M2
and
A3:
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
; M1 = M2
A4:
dom M1 = dom M2
by A1, FINSEQ_3:29;
for k being Nat st k in dom M1 holds
M1 . k = M2 . k
proof
let k be
Nat;
( k in dom M1 implies M1 . k = M2 . k )
A5:
len M1 >= 0
by NAT_1:2;
assume A6:
k in dom M1
;
M1 . k = M2 . k
then A7:
M1 . k in rng M1
by FUNCT_1:def 3;
rng M1 c= D *
by FINSEQ_1:def 4;
then reconsider p =
M1 . k as
FinSequence of
D by A7, FINSEQ_1:def 11;
M1 <> {}
by A6;
then A8:
len M1 > 0
by A5, XXREAL_0:1;
then
M1 is
Matrix of
len M1,
width M1,
D
by Th20;
then A9:
len p = width M1
by A7, Def3;
A10:
M2 . k in rng M2
by A4, A6, FUNCT_1:def 3;
rng M2 c= D *
by FINSEQ_1:def 4;
then reconsider q =
M2 . k as
FinSequence of
D by A10, FINSEQ_1:def 11;
M2 is
Matrix of
len M1,
width M1,
D
by A1, A2, A8, Th20;
then A11:
len q = width M1
by A10, Def3;
for
l being
Nat st 1
<= l &
l <= len p holds
p . l = q . l
proof
let l be
Nat;
( 1 <= l & l <= len p implies p . l = q . l )
A12:
rng p c= D
by FINSEQ_1:def 4;
assume
( 1
<= l &
l <= len p )
;
p . l = q . l
then A13:
l in Seg (width M1)
by A9, FINSEQ_1:1;
then
l in dom p
by A9, FINSEQ_1:def 3;
then
p . l in rng p
by FUNCT_1:def 3;
then reconsider a =
p . l as
Element of
D by A12;
A14:
rng q c= D
by FINSEQ_1:def 4;
l in dom q
by A11, A13, FINSEQ_1:def 3;
then
q . l in rng q
by FUNCT_1:def 3;
then reconsider b =
q . l as
Element of
D by A14;
[k,l] in Indices M2
by A2, A4, A6, A13, ZFMISC_1:87;
then A15:
M2 * (
k,
l)
= b
by Def6;
[k,l] in Indices M1
by A6, A13, ZFMISC_1:87;
then A16:
M1 * (
k,
l)
= a
by Def6;
[k,l] in [:(dom M1),(Seg (width M1)):]
by A6, A13, ZFMISC_1:87;
hence
p . l = q . l
by A3, A16, A15;
verum
end;
hence
M1 . k = M2 . k
by A9, A11, FINSEQ_1:14;
verum
end;
hence
M1 = M2
by A4, FINSEQ_1:13; verum