deffunc H₁( set ) -> Real = max+ (F . $1);
for f, g being PartFunc of D,REAL st dom f = dom F & ( for c being Element of D st c in dom f holds
f . c = H₁(c) ) & dom g = dom F & ( for c being Element of D st c in dom g holds
g . c = H₁(c) ) holds
f = g from SEQ_1:sch 4();
hence for b₁, b₂ being PartFunc of D,REAL st dom b₁ = dom F & ( for d being Element of D st d in dom b₁ holds
b₁ . d = max+ (F . d) ) & dom b₂ = dom F & ( for d being Element of D st d in dom b₂ holds
b₂ . d = max+ (F . d) ) holds
b₁ = b₂ ; :: thesis: verum