set M = Sum (Width F);
set N = Sum (Len F);
set L = Len F;
set W = Width F;
defpred S₁[ Nat, Nat, Element of D] means ( ( ( $2 <= Sum ((Width F) | ((min ((Len F),$1)) -' 1)) or $2 > Sum ((Width F) | (min ((Len F),$1))) ) implies $3 = d ) & ( Sum ((Width F) | ((min ((Len F),$1)) -' 1)) < $2 & $2 <= Sum ((Width F) | (min ((Len F),$1))) implies $3 = (F . (min ((Len F),$1))) * (($1 -' (Sum ((Len F) | ((min ((Len F),$1)) -' 1)))),($2 -' (Sum ((Width F) | ((min ((Len F),$1)) -' 1))))) ) );
A1: for i, j being Nat st [i,j] in [:(Seg (Sum (Len F))),(Seg (Sum (Width F))):] holds
ex x being Element of D st S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (Sum (Len F))),(Seg (Sum (Width F))):] implies ex x being Element of D st S₁[i,j,x] )
assume [i,j] in [:(Seg (Sum (Len F))),(Seg (Sum (Width F))):] ; :: thesis: ex x being Element of D st S₁[i,j,x]

per cases ( 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))) ) ) ;

suppose A2: ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) ; :: thesis: ex x being Element of D st S₁[i,j,x]

take d ; :: thesis: S₁[i,j,d]
thus S₁[i,j,d] by A2; :: thesis: verum

end;

suppose A3: ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) ) ; :: thesis: ex x being Element of D st S₁[i,j,x]

take (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ; :: thesis: S₁[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)))))]
thus S₁[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 A3; :: thesis: verum

end;

end;

end;

consider MM being Matrix of Sum (Len F), Sum (Width F),D such that
A4: for i, j being Nat st [i,j] in Indices MM holds
S₁[i,j,MM * (i,j)] from MATRIX_0:sch 2(A1);
take MM ; :: thesis: ( len MM = Sum (Len F) & width MM = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices MM holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies MM * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies MM * (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))))) ) ) ) )

per cases ( Sum (Len F) = 0 or Sum (Len F) > 0 ) ;

suppose A5: Sum (Len F) = 0 ; :: thesis: ( len MM = Sum (Len F) & width MM = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices MM holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies MM * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies MM * (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))))) ) ) ) )

then Sum (Width F) = 0 by Th13;
hence ( len MM = Sum (Len F) & width MM = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices MM holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies MM * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies MM * (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 A5, MATRIX_0:22; :: thesis: verum

end;

suppose Sum (Len F) > 0 ; :: thesis: ( len MM = Sum (Len F) & width MM = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices MM holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies MM * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies MM * (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))))) ) ) ) )

hence ( len MM = Sum (Len F) & width MM = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices MM holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies MM * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies MM * (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 A4, MATRIX_0:23; :: thesis: verum

end;

end;