let n be non empty Element of NAT ; :: thesis: 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); :: thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )

hereby :: thesis: ( ( 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 ; :: thesis: 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 :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (Proj (i,n)) * h is continuous )
assume A2: i in Seg n ; :: thesis: (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;

now :: thesis: for x0 being real number st x0 in dom ((Proj (i,n)) * h) holds
(Proj (i,n)) * h is_continuous_in x0

let x0 be real number ; :: thesis: ( x0 in dom ((Proj (i,n)) * h) implies (Proj (i,n)) * h is_continuous_in x0 )
assume x0 in dom ((Proj (i,n)) * h) ; :: thesis: (Proj (i,n)) * h is_continuous_in x0
then h is_continuous_in x0 by A1, A4, NFCONT_3:def 2;
hence (Proj (i,n)) * h is_continuous_in x0 by A2, Th46; :: thesis: verum

end;

hence (Proj (i,n)) * h is continuous by NFCONT_3:def 2; :: thesis: verum

end;

end;

assume A5: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous ; :: thesis: h is continuous
let x0 be real number ; :: according to NFCONT_3:def 2 :: thesis: ( not x0 in dom h or h is_continuous_in x0 )
assume A6: x0 in dom h ; :: thesis: h is_continuous_in x0

now :: thesis: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0

let i be Element of NAT ; :: thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 )
assume A7: i in Seg n ; :: thesis: (Proj (i,n)) * h is_continuous_in x0
A8: 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 A9: dom ((Proj (i,n)) * h) = dom h by A8, RELAT_1:27;
(Proj (i,n)) * h is continuous by A5, A7;
hence (Proj (i,n)) * h is_continuous_in x0 by A6, A9, NFCONT_3:def 2; :: thesis: verum

end;

hence h is_continuous_in x0 by Th46; :: thesis: verum