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 )
assume A5:
k in dom M1
;
M1 . k = M2 . k
then A6:
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 A6, FINSEQ_1:def 11;
M1 <> {}
by A5;
then A7:
len M1 > 0
;
then
M1 is
Matrix of
len M1,
width M1,
D
by Th20;
then A8:
len p = width M1
by A6, Def2;
A9:
M2 . k in rng M2
by A4, A5, FUNCT_1:def 3;
rng M2 c= D *
by FINSEQ_1:def 4;
then reconsider q =
M2 . k as
FinSequence of
D by A9, FINSEQ_1:def 11;
M2 is
Matrix of
len M1,
width M1,
D
by A1, A2, A7, Th20;
then A10:
len q = width M1
by A9, Def2;
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 )
A11:
rng p c= D
by FINSEQ_1:def 4;
assume
( 1
<= l &
l <= len p )
;
p . l = q . l
then A12:
l in Seg (width M1)
by A8, FINSEQ_1:1;
then
l in dom p
by A8, 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 A11;
A13:
rng q c= D
by FINSEQ_1:def 4;
l in dom q
by A10, A12, 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 A13;
[k,l] in Indices M2
by A2, A4, A5, A12, ZFMISC_1:87;
then A14:
M2 * (
k,
l)
= b
by Def5;
[k,l] in Indices M1
by A5, A12, ZFMISC_1:87;
then A15:
M1 * (
k,
l)
= a
by Def5;
[k,l] in [:(dom M1),(Seg (width M1)):]
by A5, A12, ZFMISC_1:87;
hence
p . l = q . l
by A3, A15, A14;
verum
end;
hence
M1 . k = M2 . k
by A8, A10, FINSEQ_1:14;
verum
end;
hence
M1 = M2
by A4, FINSEQ_1:13; verum