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;

A4: 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 ;
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(A4, 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 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 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 A6, MATRIX_1:23; :: 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;