:: deftheorem defines " COMBGRAS:def 11 :
for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S2 holds F " K = the point-map of F " K;