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
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