let D, E be non empty set ; :: thesis: for M being Matrix of D
for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) holds
M = L
let M be Matrix of D; :: thesis: for L being Matrix of E st len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) holds
M = L
let L be Matrix of E; :: thesis: ( len M = len L & width M = width L & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ) implies M = L )
assume that
A1: len M = len L and
A2: width M = width L and
A3: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = L * (i,j) ; :: thesis: M = L
M is Matrix of E

proof

consider n being Nat such that
A0: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n ) by MATRIX_0:9;

per cases ( len M = 0 or len M <> 0 ) ;

suppose len M = 0 ; :: thesis: M is Matrix of E

then M = {} ;
then rng M c= E * ;
hence M is Matrix of E by FINSEQ_1:def 4; :: thesis: verum

end;

suppose I0: len M <> 0 ; :: thesis: M is Matrix of E

for x being object st x in rng M holds
ex p being FinSequence of E st
( x = p & len p = n )

proof

let x be object ; :: thesis: ( x in rng M implies ex p being FinSequence of E st
( x = p & len p = n ) )
assume S1: x in rng M ; :: thesis: ex p being FinSequence of E st
( x = p & len p = n )
then consider p being FinSequence of D such that
S3: ( x = p & len p = n ) by A0;
X1: width M = n by S1, S3, MATRIX_0:def 3, I0;
for z being object st z in rng p holds
z in E

proof

let z be object ; :: thesis: ( z in rng p implies z in E )
assume z in rng p ; :: thesis: z in E
then consider j1 being object such that
S4: ( j1 in dom p & z = p . j1 ) by FUNCT_1:def 3;
S5: j1 in Seg n by S3, S4, FINSEQ_1:def 3;
reconsider j1 = j1 as Nat by S4;
consider i1 being object such that
S6: ( i1 in dom M & x = M . i1 ) by S1, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by S6;
S8: [i1,j1] in Indices M by S6, S5, X1, ZFMISC_1:87;
then consider q being FinSequence of D such that
S9: ( q = M . i1 & M * (i1,j1) = q . j1 ) by MATRIX_0:def 5;
M * (i1,j1) = L * (i1,j1) by A3, S8;
hence z in E by S3, S4, S6, S9; :: thesis: verum

end;

then rng p c= E ;
then reconsider p = p as FinSequence of E by FINSEQ_1:def 4;
take p ; :: thesis: ( x = p & len p = n )
thus ( x = p & len p = n ) by S3; :: thesis: verum

end;

hence M is Matrix of E by MATRIX_0:9; :: thesis: verum

end;

end;

end;

then reconsider L0 = M as Matrix of E ;
for i, j being Nat st [i,j] in Indices L0 holds
L0 * (i,j) = L * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices L0 implies L0 * (i,j) = L * (i,j) )
assume X3: [i,j] in Indices L0 ; :: thesis: L0 * (i,j) = L * (i,j)
then consider q being FinSequence of D such that
S9: ( q = M . i & M * (i,j) = q . j ) by MATRIX_0:def 5;
consider p being FinSequence of E such that
T9: ( p = L0 . i & L0 * (i,j) = p . j ) by MATRIX_0:def 5, X3;
thus L0 * (i,j) = L * (i,j) by A3, S9, T9, X3; :: thesis: verum

end;

hence M = L by A1, A2, MATRIX_0:21; :: thesis: verum