theorem :: PARTFUN1:32

for f being Function holds f = <:f,(dom f),(rng f):> ;