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