:: deftheorem defines . COMBGRAS:def 6 :
for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for a being POINT of S1 holds F . a = the point-map of F . a;