let x0 be real number ; :: thesis: for n being non empty 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 empty 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 AS: 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 X1: 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 P1: ( 1 <= i & i <= n ) by FINSEQ_1:1;
P20: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then P2: dom ((proj (i,n)) * h) = dom h by P20, RELAT_1:27;
proj (i,n) is_continuous_in h /. x0 by P1, X0;
hence (proj (i,n)) * h is_continuous_in x0 by P2, AS, X1, Th12X; :: thesis: verum

end;

end;

assume AS11: ( 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 number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r ) )

proof

let r0 be Real; :: thesis: ( 0 < r0 implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) ) )
assume AX1: 0 < r0 ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
|.((h /. x1) - (h /. x0)).| < r0 ) )
set r = r0 / 2;
AX11: 0 < r0 / 2 by AX1, XREAL_1:215;
defpred S₁[ Nat, real number ] means ( 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
|.((((proj ($1,n)) * h) . x1) - (((proj ($1,n)) * h) . x0)).| < (r0 / 2) / n ) );
BB1: 0 < (r0 / 2) / n by AX11, XREAL_1:139;
BB2: 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 BX0: j in Seg n ; :: thesis: ex x being Element of REAL st S₁[j,x]
U3: (proj (j,n)) * h is_continuous_in x0 by AS11, BX0;
P20: dom (proj (j,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n ;
then P21: dom ((proj (j,n)) * h) = dom h by P20, RELAT_1:27;
consider sj being real number such that
BX3: ( 0 < sj & ( for x1 being real number st x1 in dom ((proj (j,n)) * h) & abs (x1 - x0) < sj holds
|.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) ) by U3, BB1, FCONT_1:3;
sj is Real by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[j,x] by BX3, P21; :: thesis: verum

end;

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

now

let x1 be real number ; :: thesis: ( x1 in dom h & abs (x1 - x0) < s implies |.((h /. x1) - (h /. x0)).| < r0 )
assume BX3: ( x1 in dom h & abs (x1 - x0) < s ) ; :: thesis: |.((h /. x1) - (h /. x0)).| < r0

now

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 BX1: j in Seg n by FINSEQ_1:1;
then s0 . j in rng s0 by BB3, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def 7;
then abs (x1 - x0) < s0 . j by BX3, XXREAL_0:2;
then X100: |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n by BX1, BX3, BB3;
C1: ((proj (j,n)) * h) . x1 = (proj (j,n)) . (h . x1) by BX3, FUNCT_1:13
.= (proj (j,n)) . (h /. x1) by BX3, PARTFUN1:def 6 ;
((proj (j,n)) * h) . x0 = (proj (j,n)) . (h . x0) by AS11, FUNCT_1:13
.= (proj (j,n)) . (h /. x0) by AS11, PARTFUN1:def 6 ;
hence |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n by X100, C1, PDIFF_8:12; :: thesis: verum

end;

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

end;

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

end;

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