let n be Nat; :: thesis: for S1, S2 being non empty 1-sorted
for X being Matrix of n,S2
for Y being Matrix of n,S1 holds
( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )
let S1, S2 be non empty 1-sorted ; :: thesis: for X being Matrix of n,S2
for Y being Matrix of n,S1 holds
( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )
let X be Matrix of n,S2; :: thesis: for Y being Matrix of n,S1 holds
( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )
let Y be Matrix of n,S1; :: thesis: ( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )
thus ( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) implies X = Y ) :: thesis: ( X = Y implies for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) )

proof

assume A1: for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ; :: thesis: X = Y
A2: dom X = Seg (len X) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:25
.= Seg (len Y) by MATRIX_0:25
.= dom Y by FINSEQ_1:def 3 ;
for i being Nat st i in dom X holds
X . i = Y . i

proof

let i be Nat; :: thesis: ( i in dom X implies X . i = Y . i )
assume A3: i in dom X ; :: thesis: X . i = Y . i

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: X . i = Y . i

then len X = 0 by MATRIX_0:25;
then {} = Seg (len X)
.= dom X by FINSEQ_1:def 3 ;
hence X . i = Y . i by A3; :: thesis: verum

end;

suppose n > 0 ; :: thesis: X . i = Y . i

then A4: ( len X > 0 & len Y > 0 ) by MATRIX_0:25;
A5: X . i in rng X by A3, FUNCT_1:def 3;
then reconsider p = X . i as FinSequence of S2 by FINSEQ_1:def 11;
A6: Y . i in rng Y by A2, A3, FUNCT_1:def 3;
then reconsider q = Y . i as FinSequence of S1 by FINSEQ_1:def 11;
A7: dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (width X) by A5, A4, MATRIX_0:def 3
.= Seg n by MATRIX_0:24
.= Seg (width Y) by MATRIX_0:24
.= Seg (len q) by A6, A4, MATRIX_0:def 3
.= dom q by FINSEQ_1:def 3 ;
for j being Nat st j in dom p holds
p . j = q . j

proof

let j be Nat; :: thesis: ( j in dom p implies p . j = q . j )
assume A8: j in dom p ; :: thesis: p . j = q . j
A9: [i,j] in Indices X

proof

dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (width X) by A5, A4, MATRIX_0:def 3 ;
then [i,j] in [:(dom X),(Seg (width X)):] by A3, A8, ZFMISC_1:87;
hence [i,j] in Indices X by MATRIX_0:def 4; :: thesis: verum

end;

Indices X = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices Y by MATRIX_0:24 ;
then A10: ex q9 being FinSequence of S1 st
( q9 = Y . i & Y * (i,j) = q9 . j ) by A9, MATRIX_0:def 5;
ex p9 being FinSequence of S2 st
( p9 = X . i & X * (i,j) = p9 . j ) by A9, MATRIX_0:def 5;
hence p . j = q . j by A1, A9, A10; :: thesis: verum

end;

hence X . i = Y . i by A7, FINSEQ_1:13; :: thesis: verum

end;

end;

end;

hence X = Y by A2, FINSEQ_1:13; :: thesis: verum

end;

assume A11: X = Y ; :: thesis: for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices X implies X * (i,j) = Y * (i,j) )
assume A12: [i,j] in Indices X ; :: thesis: X * (i,j) = Y * (i,j)
then consider q being FinSequence of S1 such that
A13: ( q = Y . i & Y * (i,j) = q . j ) by A11, MATRIX_0:def 5;
consider p being FinSequence of S2 such that
A14: ( p = X . i & X * (i,j) = p . j ) by A12, MATRIX_0:def 5;
thus X * (i,j) = Y * (i,j) by A11, A13, A14; :: thesis: verum