deffunc H₁( Element of CNS1) -> Element of REAL = ||.(f /. $1).||;
for f1, f2 being PartFunc of the carrier of CNS1,REAL st dom f1 = dom f & ( for c being Element of CNS1 st c in dom f1 holds
f1 . c = H₁(c) ) & dom f2 = dom f & ( for c being Element of CNS1 st c in dom f2 holds
f2 . c = H₁(c) ) holds
f1 = f2 from SEQ_1:sch 4();
hence for b₁, b₂ being PartFunc of the carrier of CNS1,REAL st dom b₁ = dom f & ( for c being Point of CNS1 st c in dom b₁ holds
b₁ . c = ||.(f /. c).|| ) & dom b₂ = dom f & ( for c being Point of CNS1 st c in dom b₂ holds
b₂ . c = ||.(f /. c).|| ) holds
b₁ = b₂ ; :: thesis: verum