deffunc H₁( Element of NAT ) -> Function of NAT,ExtREAL = (G . $1) vol ;
thus for F1, F2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds F1 . n = H₁(n) ) & ( for n being Element of NAT holds F2 . n = H₁(n) ) holds
F1 = F2 from BINOP_2:sch 1(); :: thesis: verum