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