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
A7: len M1 = Sum (Len F) and
A8: width M1 = Sum (Width F) and
A9: 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
A10: len M2 = Sum (Len F) and
A11: width M2 = Sum (Width F) and
A12: 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
A13: Indices M1 = [:(Seg (len M1)),(Seg (width M1)):] by FINSEQ_1:def 3
.= Indices M2 by A7, A8, A10, A11, FINSEQ_1:def 3 ;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A14: [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 A9, A12, A13, A14;
hence M1 * (i,j) = M2 * (i,j) ; :: thesis: verum

end;

hence M1 = M2 by A7, A8, A10, A11, MATRIX_1:21; :: thesis: verum