set W = Width F;
set L = Len F;
let M1, M2 be Matrix of D; :: thesis: ( len M1 = Sum (Len F) & width M1 = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices M1 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies M1 * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies M1 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) ) & len M2 = Sum (Len F) & width M2 = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices M2 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies M2 * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies M2 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) ) implies M1 = M2 )
assume that
A6: len M1 = Sum (Len F) and
A7: width M1 = Sum (Width F) and
A8: for i, j being Nat st [i,j] in Indices M1 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies M1 * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies M1 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) and
A9: len M2 = Sum (Len F) and
A10: width M2 = Sum (Width F) and
A11: for i, j being Nat st [i,j] in Indices M2 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies M2 * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies M2 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) ; :: thesis: M1 = M2
A12: Indices M1 = [:(Seg (len M1)),(Seg (width M1)):] by FINSEQ_1:def 3
.= Indices M2 by A6, A7, A9, A10, FINSEQ_1:def 3 ;

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 A13: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) or ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) ) ) ;
then ( ( M1 * (i,j) = d & M2 * (i,j) = d ) or ( M1 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) & M2 * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) by A8, A11, A12, A13;
hence M1 * (i,j) = M2 * (i,j) ; :: thesis: verum

end;

hence M1 = M2 by A6, A7, A9, A10, MATRIX_0:21; :: thesis: verum