let n be non empty Element of NAT ; :: thesis: for h being PartFunc of REAL,(REAL 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 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 P1: 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 P2: i in Seg n ; :: thesis: (proj (i,n)) * h is continuous
P20: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then P21: dom ((proj (i,n)) * h) = dom h by P20, RELAT_1:27;

now

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 P1, P21, Def2;
hence (proj (i,n)) * h is_continuous_in x0 by P2, X1; :: thesis: verum

end;

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

end;

end;

assume Q1: 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_4:def 5 :: thesis: ( x0 in dom h implies h is_continuous_in x0 )
assume A2: x0 in dom h ; :: thesis: h is_continuous_in x0

now

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume P2: i in Seg n ; :: thesis: (proj (i,n)) * h is_continuous_in x0
P20: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then P21: dom ((proj (i,n)) * h) = dom h by P20, RELAT_1:27;
(proj (i,n)) * h is continuous by Q1, P2;
hence (proj (i,n)) * h is_continuous_in x0 by A2, P21, FCONT_1:def 2; :: thesis: verum

end;

hence h is_continuous_in x0 by A2, X1; :: thesis: verum