let D be non empty set ; :: thesis: 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; :: thesis: ( 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
; :: thesis: M1 = M2
A4:
dom M1 = dom M2
by A1, FINSEQ_3:31;
for k being Nat st k in dom M1 holds
M1 . k = M2 . k
proof
let k be
Nat;
:: thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A5:
k in dom M1
;
:: thesis: M1 . k = M2 . k
then A6:
(
M1 . k in rng M1 &
M2 . k in rng M2 )
by A4, FUNCT_1:def 5;
A7:
(
rng M1 c= D * &
rng M2 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
(
len M1 <> 0 &
len M1 >= 0 )
by NAT_1:2;
then A8:
len M1 > 0
by XXREAL_0:1;
then
M1 is
Matrix of
len M1,
width M1,
D
by Th20;
then A9:
len p = width M1
by A6, Def3;
reconsider q =
M2 . k as
FinSequence of
D by A6, A7, FINSEQ_1:def 11;
M2 is
Matrix of
len M1,
width M1,
D
by A1, A2, A8, Th20;
then A10:
len q = width M1
by A6, Def3;
for
l being
Nat st 1
<= l &
l <= len p holds
p . l = q . l
proof
let l be
Nat;
:: thesis: ( 1 <= l & l <= len p implies p . l = q . l )
assume
( 1
<= l &
l <= len p )
;
:: thesis: p . l = q . l
then A11:
l in Seg (width M1)
by A9, FINSEQ_1:3;
then
(
l in dom p &
l in dom q )
by A9, A10, FINSEQ_1:def 3;
then A12:
(
p . l in rng p &
rng p c= D &
q . l in rng q &
rng q c= D )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider a =
p . l as
Element of
D ;
reconsider b =
q . l as
Element of
D by A12;
A13:
(
[k,l] in [:(dom M1),(Seg (width M1)):] &
[k,l] in [:(dom M2),(Seg (width M2)):] )
by A2, A4, A5, A11, ZFMISC_1:106;
(
[k,l] in Indices M1 &
[k,l] in Indices M2 )
by A2, A4, A5, A11, ZFMISC_1:106;
then
(
M1 * k,
l = a &
M2 * k,
l = b )
by Def6;
hence
p . l = q . l
by A3, A13;
:: thesis: verum
end;
hence
M1 . k = M2 . k
by A9, A10, FINSEQ_1:18;
:: thesis: verum
end;
hence
M1 = M2
by A4, FINSEQ_1:17; :: thesis: verum