theorem Th16: :: COMBGRAS:16

for S1, S2 being IncProjStr
for F1, F2 being IncProjMap over S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) holds
IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)