:: deftheorem defines <>* PDIFF_1:def 2 :
for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1));