theorem Th43: :: NFCONT_4:43

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