let x0 be Real; :: thesis: 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 ) ) )
let n be non zero Element of NAT ; :: thesis: 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 ) ) )
let h be PartFunc of REAL,(REAL n); :: thesis: ( 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 ) ) )

hereby :: thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 )

assume A1: h is_continuous_in x0 ; :: thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) )
hence A2: x0 in dom h by Th3; :: thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0
thus for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )
assume i in Seg n ; :: thesis: (proj (i,n)) * h is_continuous_in x0
then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A4: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then A5: dom ((proj (i,n)) * h) = dom h by A4, RELAT_1:27;
proj (i,n) is_continuous_in h /. x0 by A3, Th42;
hence (proj (i,n)) * h is_continuous_in x0 by A5, A1, A2, Th22; :: thesis: verum

end;

end;

assume A6: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) ; :: thesis: h is_continuous_in x0
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r ) )

proof

let r0 be Real; :: thesis: ( 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) ) )
assume A7: 0 < r0 ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
set r = r0 / 2;
A8: 0 < r0 / 2 by A7, XREAL_1:215;
defpred S₁[ Nat, Real] means ( 0 < $2 & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < $2 holds
|.((((proj ($1,n)) * h) . x1) - (((proj ($1,n)) * h) . x0)).| < (r0 / 2) / n ) );
A9: 0 < (r0 / 2) / n by A8, XREAL_1:139;
A10: for j being Nat st j in Seg n holds
ex x being Element of REAL st S₁[j,x]

proof

let j be Nat; :: thesis: ( j in Seg n implies ex x being Element of REAL st S₁[j,x] )
assume A11: j in Seg n ; :: thesis: ex x being Element of REAL st S₁[j,x]
A12: (proj (j,n)) * h is_continuous_in x0 by A6, A11;
A13: dom (proj (j,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then A14: dom ((proj (j,n)) * h) = dom h by A13, RELAT_1:27;
consider sj being Real such that
A15: ( 0 < sj & ( for x1 being Real st x1 in dom ((proj (j,n)) * h) & |.(x1 - x0).| < sj holds
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) ) by A12, A9, FCONT_1:3;
sj in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[j,x] by A15, A14; :: thesis: verum

end;

consider s0 being FinSequence of REAL such that
A16: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,s0 . k] ) ) from FINSEQ_1:sch 5(A10);
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A16, FUNCT_1:3;
rng s0 is finite by A16, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A17: min rs0 in rng s0 by XXREAL_2:def 7;
reconsider s = min rs0 as Real ;
take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
ex i1 being object st
( i1 in dom s0 & s = s0 . i1 ) by A17, FUNCT_1:def 3;
hence 0 < s by A16; :: thesis: for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0

now :: thesis: for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0

let x1 be Real; :: thesis: ( x1 in dom h & |.(x1 - x0).| < s implies |.((h /. x1) - (h /. x0)).| < r0 )
assume A18: ( x1 in dom h & |.(x1 - x0).| < s ) ; :: thesis: |.((h /. x1) - (h /. x0)).| < r0

now :: thesis: for j being Element of NAT st 1 <= j & j <= n holds
|.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n

let j be Element of NAT ; :: thesis: ( 1 <= j & j <= n implies |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n )
assume ( 1 <= j & j <= n ) ; :: thesis: |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n
then A19: j in Seg n by FINSEQ_1:1;
then s0 . j in rng s0 by A16, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def 7;
then |.(x1 - x0).| < s0 . j by A18, XXREAL_0:2;
then A20: |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n by A19, A18, A16;
A21: ((proj (j,n)) * h) . x1 = (proj (j,n)) . (h . x1) by A18, FUNCT_1:13
.= (proj (j,n)) . (h /. x1) by A18, PARTFUN1:def 6 ;
((proj (j,n)) * h) . x0 = (proj (j,n)) . (h . x0) by A6, FUNCT_1:13
.= (proj (j,n)) . (h /. x0) by A6, PARTFUN1:def 6 ;
hence |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n by A20, A21, PDIFF_8:12; :: thesis: verum

end;

then |.((h /. x1) - (h /. x0)).| <= n * ((r0 / 2) / n) by PDIFF_8:17;
then A22: |.((h /. x1) - (h /. x0)).| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A7, XREAL_1:216;
hence |.((h /. x1) - (h /. x0)).| < r0 by A22, XXREAL_0:2; :: thesis: verum

end;

hence for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
|.((h /. x1) - (h /. x0)).| < r0 ; :: thesis: verum

end;

hence h is_continuous_in x0 by A6, Th3; :: thesis: verum