set W = Width F;
set L = Len 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)))) ) );
set N = Sum (Len F);
set M = Sum (Width F);
A1: for i, j being Nat st [i,j] in [:(Seg (Sum (Len F))),(Seg (Sum (Width F))):] holds
for x1, x2 being Element of D st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A2: 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 A3: ( 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 A3; :: thesis: verum

end;

suppose A4: ( 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 b = (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,b]
thus S₁[i,j,b] by A4; :: thesis: verum

end;

end;

end;

consider MM being Matrix of Sum (Len F), Sum (Width F),D such that
A5: for i, j being Nat st [i,j] in Indices MM holds
S₁[i,j,MM * i,j] from MATRIX_1:sch 2(A1, A2);
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 A6: 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 & len MM = 0 & width MM = 0 ) by Th13, MATRIX_1:23;
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, A6; :: 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 A5, MATRIX_1:24; :: thesis: verum

end;

end;