theorem Th46: :: NFCONT_4:46

for x0 being Real
for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )