let M1, M2 be Matrix of D; :: thesis: ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * i,j = M * j,i ) & len M2 = width M & ( for i, j being Nat holds
( [i,j] in Indices M2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M2 * i,j = M * j,i ) implies M1 = M2 )
assume that
A5: len M1 = width M and
A6: for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) and
A7: for i, j being Nat st [j,i] in Indices M holds
M1 * i,j = M * j,i and
A8: len M2 = width M and
A9: for i, j being Nat holds
( [i,j] in Indices M2 iff [j,i] in Indices M ) and
A10: for i, j being Nat st [j,i] in Indices M holds
M2 * i,j = M * j,i ; :: thesis: M1 = M2

A11: now

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * i,j = M2 * i,j )
assume [i,j] in Indices M1 ; :: thesis: M1 * i,j = M2 * i,j
then A12: [j,i] in Indices M by A6;
then M1 * i,j = M * j,i by A7;
hence M1 * i,j = M2 * i,j by A10, A12; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( ( [x,y] in [:(dom M1),(Seg (width M1)):] implies [x,y] in [:(dom M2),(Seg (width M2)):] ) & ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] ) )
thus ( [x,y] in [:(dom M1),(Seg (width M1)):] implies [x,y] in [:(dom M2),(Seg (width M2)):] ) :: thesis: ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] )

proof

assume A13: [x,y] in [:(dom M1),(Seg (width M1)):] ; :: thesis: [x,y] in [:(dom M2),(Seg (width M2)):]
then x in dom M1 by ZFMISC_1:106;
then reconsider i = x as Element of NAT ;
y in Seg (width M1) by A13, ZFMISC_1:106;
then reconsider j = y as Element of NAT ;
[j,i] in Indices M by A6, A13;
hence [x,y] in [:(dom M2),(Seg (width M2)):] by A9; :: thesis: verum

end;

thus ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] ) :: thesis: verum

proof

assume A14: [x,y] in [:(dom M2),(Seg (width M2)):] ; :: thesis: [x,y] in [:(dom M1),(Seg (width M1)):]
then x in dom M2 by ZFMISC_1:106;
then reconsider i = x as Element of NAT ;
y in Seg (width M2) by A14, ZFMISC_1:106;
then reconsider j = y as Element of NAT ;
[j,i] in Indices M by A9, A14;
hence [x,y] in [:(dom M1),(Seg (width M1)):] by A6; :: thesis: verum

end;

end;

then A15: [:(dom M1),(Seg (width M1)):] = [:(dom M2),(Seg (width M2)):] by ZFMISC_1:108;

A16: now

assume A17: len M1 <> 0 ; :: thesis: ( len M1 = len M2 & width M1 = width M2 )
then Seg (len M2) <> {} by A5, A8;
then A18: dom M2 <> {} by FINSEQ_1:def 3;

now

per cases ( Seg (width M1) <> {} or Seg (width M1) = {} ) ;

suppose A19: Seg (width M1) <> {} ; :: thesis: width M1 = width M2

Seg (len M1) <> {} by A17;
then dom M1 <> {} by FINSEQ_1:def 3;
then Seg (width M1) = Seg (width M2) by A15, A19, ZFMISC_1:134;
hence width M1 = width M2 by FINSEQ_1:8; :: thesis: verum

end;

suppose A20: Seg (width M1) = {} ; :: thesis: width M1 = width M2

then [:(dom M2),(Seg (width M2)):] = {} by A15, ZFMISC_1:113;
then Seg (width M2) = {} by A18, ZFMISC_1:113;
hence width M1 = width M2 by A20, FINSEQ_1:8; :: thesis: verum

end;

end;

end;

hence ( len M1 = len M2 & width M1 = width M2 ) by A5, A8; :: thesis: verum

end;

( len M1 = 0 implies ( len M2 = 0 & width M1 = 0 & width M2 = 0 ) ) by A5, A8, Def4;
hence M1 = M2 by A16, A11, Th21; :: thesis: verum