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
A6: len M1 = width M and
A7: for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) and
A8: for i, j being Nat st [j,i] in Indices M holds
M1 * (i,j) = M * (j,i) and
A9: len M2 = width M and
A10: for i, j being Nat holds
( [i,j] in Indices M2 iff [j,i] in Indices M ) and
A11: for i, j being Nat st [j,i] in Indices M holds
M2 * (i,j) = M * (j,i) ; :: thesis: M1 = M2

A12: now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

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 A13: [j,i] in Indices M by A7;
then M1 * (i,j) = M * (j,i) by A8;
hence M1 * (i,j) = M2 * (i,j) by A11, A13; :: thesis: verum

end;

now :: thesis: for x, y being object holds
( ( [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)):] ) )

let x, y be object ; :: 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 A14: [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:87;
then reconsider i = x as Nat ;
y in Seg (width M1) by A14, ZFMISC_1:87;
then reconsider j = y as Nat ;
[j,i] in Indices M by A7, A14;
hence [x,y] in [:(dom M2),(Seg (width M2)):] by A10; :: 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 A15: [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:87;
then reconsider i = x as Nat ;
y in Seg (width M2) by A15, ZFMISC_1:87;
then reconsider j = y as Nat ;
[j,i] in Indices M by A10, A15;
hence [x,y] in [:(dom M1),(Seg (width M1)):] by A7; :: thesis: verum

end;

end;

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

A17: now :: thesis: ( len M1 <> 0 implies ( len M1 = len M2 & width M1 = width M2 ) )

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

now :: thesis: width M1 = width M2

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

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

Seg (len M1) <> {} by A18;
then dom M1 <> {} by FINSEQ_1:def 3;
then Seg (width M1) = Seg (width M2) by A16, A20, ZFMISC_1:110;
hence width M1 = width M2 by FINSEQ_1:6; :: thesis: verum

end;

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

then [:(dom M2),(Seg (width M2)):] = {} by A16, ZFMISC_1:90;
then Seg (width M2) = {} by A19, ZFMISC_1:90;
hence width M1 = width M2 by A21, FINSEQ_1:6; :: thesis: verum

end;

end;

end;

hence ( len M1 = len M2 & width M1 = width M2 ) by A6, A9; :: thesis: verum

end;

( len M1 = 0 implies ( len M2 = 0 & width M1 = 0 & width M2 = 0 ) ) by A6, A9, Def3;
hence M1 = M2 by A17, A12, Th21; :: thesis: verum