theorem :: HILBERT3:18

for g being Function holds {} .. g = {}