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