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