for x0 being Real
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
I is_continuous_in x0