let n be non zero Element of NAT ; for h being PartFunc of REAL,(REAL-NS n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
let h be PartFunc of REAL,(REAL-NS n); ( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
hereby ( ( for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ) implies h is continuous )
assume A1:
h is
continuous
;
for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous thus
for
i being
Element of
NAT st
i in Seg n holds
(Proj (i,n)) * h is
continuous
verumproof
let i be
Element of
NAT ;
( i in Seg n implies (Proj (i,n)) * h is continuous )
assume A2:
i in Seg n
;
(Proj (i,n)) * h is continuous
A3:
dom (Proj (i,n)) = the
carrier of
(REAL-NS n)
by FUNCT_2:def 1;
rng h c= the
carrier of
(REAL-NS n)
;
then A4:
dom ((Proj (i,n)) * h) = dom h
by A3, RELAT_1:27;
for
x0 being
Real st
x0 in dom ((Proj (i,n)) * h) holds
(Proj (i,n)) * h is_continuous_in x0
by A2, Th46, A1, A4;
hence
(Proj (i,n)) * h is
continuous
;
verum
end;
end;
assume A5:
for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous
; h is continuous
let x0 be Real; NFCONT_3:def 2 ( not x0 in dom h or h is_continuous_in x0 )
assume A6:
x0 in dom h
; h is_continuous_in x0
hence
h is_continuous_in x0
by Th46; verum