let x0 be real number ; :: thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff 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-NS n) holds
( h is_continuous_in x0 iff 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-NS n); :: thesis: ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )

hereby :: thesis: ( ( 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: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0
then A2: x0 in dom h by NFCONT_3:7;
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)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng h c= the carrier of (REAL-NS 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, Th45;
hence (Proj (i,n)) * h is_continuous_in x0 by A2, A5, A1, NFCONT_3:15; :: thesis: verum

end;

end;

assume A6: 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
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then (Proj (1,n)) * h is_continuous_in x0 by A6;
then A7: x0 in dom ((Proj (1,n)) * h) by NFCONT_3:8;
A8: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25;
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 ) ) )
set r = r0 / 2;
assume A9: 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 ) )
then A10: 0 < r0 / 2 by XREAL_1:215;
defpred S₁[ set , real number ] means ex j being Element of NAT st
( $1 = j & 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) );
A11: 0 < (r0 / 2) / n by A10, XREAL_1:139;
A12: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S₁[j0,x]

proof

let j0 be Nat; :: thesis: ( j0 in Seg n implies ex x being Element of REAL st S₁[j0,x] )
assume A13: j0 in Seg n ; :: thesis: ex x being Element of REAL st S₁[j0,x]
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
A14: (Proj (j,n)) * h is_continuous_in x0 by A6, A13;
A15: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng h c= the carrier of (REAL-NS n) ;
then A16: dom ((Proj (j,n)) * h) = dom h by A15, RELAT_1:27;
consider sj being real number such that
A17: ( 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 A14, A11, NFCONT_3:8;
sj is Real by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[j0,x] by A17, A16; :: thesis: verum

end;

consider s0 being FinSequence of REAL such that
A18: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,s0 . k] ) ) from FINSEQ_1:sch 5(A12);
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A18, FUNCT_1:3;
rng s0 is finite by A18, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
A19: 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 ) )
consider i1 being set such that
A20: ( i1 in dom s0 & s = s0 . i1 ) by A19, FUNCT_1:def 3;
ex j being Element of NAT st
( i1 = j & 0 < s0 . i1 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . i1 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18, A20;
hence 0 < s by A20; :: thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r0
let x1 be real number ; :: thesis: ( x1 in dom h & abs (x1 - x0) < s implies ||.((h /. x1) - (h /. x0)).|| < r0 )
assume A21: ( x1 in dom h & abs (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 A22: j in Seg n by FINSEQ_1:1;
then consider jj being Element of NAT such that
A23: ( jj = j & 0 < s0 . j & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . j holds
||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18;
s0 . j in rng s0 by A22, A18, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def 7;
then abs (x1 - x0) < s0 . j by A21, XXREAL_0:2;
then A24: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by A23, A21;
A25: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then A26: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by A21, PARTFUN2:4;
((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by A25, A8, A7, PARTFUN2:4;
hence ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by A24, A26, PDIFF_8:11; :: thesis: verum

end;

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

end;

hence h is_continuous_in x0 by A8, A7, NFCONT_3:8; :: thesis: verum