abs f = |.f.| ;
hence |.f.| is PartFunc of C,NAT ; :: thesis: verum