let E, F be RealNormSpace; :: thesis:
let g be PartFunc of E,F; :: thesis:
let S be Subset of E; :: thesis:
assume that
A1: g is_continuous_on S and
A2: dom g = S ; :: thesis:
defpred S₁[ object , object ] means ex t being Point of E st
( t = $1 & $2 = [t,(g . t)] );
A3: for x being object st x in S holds
ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] )

let x be object ; :: thesis:
assume A4: x in S ; :: thesis:
then reconsider t = x as Point of E ;
take y = [t,(g . t)]; :: thesis:
g . t in rng g by A2, A4, FUNCT_1:3;
then reconsider q = g . t as Point of F ;
[t,q] is Point of [:E,F:] ;
hence ( y in the carrier of [:E,F:] & S₁[x,y] ) ; :: thesis:

end;

consider H being Function of S,[:E,F:] such that
A6: for z being object st z in S holds
S₁[z,H . z] from FUNCT_2:sch 1(A3);
A7: dom H = S by FUNCT_2:def 1;
rng H c= the carrier of [:E,F:] ;
then H in PFuncs ( the carrier of E, the carrier of [:E,F:]) by A7, PARTFUN1:def 3;
then reconsider H = H as PartFunc of E,[:E,F:] by PARTFUN1:46;
take H ; :: thesis:
thus dom H = S by FUNCT_2:def 1; :: thesis:
thus A11: for s being Point of E st s in S holds
H . s = [s,(g . s)] :: thesis:

let s be Point of E; :: thesis:
assume s in S ; :: thesis:
then ex t being Point of E st
( t = s & H . s = [t,(g . t)] ) by A6;
hence H . s = [s,(g . s)] ; :: thesis:

end;

for x0 being Point of E
for r being Real st x0 in S & 0 < r holds
ex pq being Real st
( 0 < pq & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )

let x0 be Point of E; :: thesis:
let r be Real; :: thesis:
assume A12: ( x0 in S & 0 < r ) ; :: thesis:
then A14: g . x0 in rng g by A2, FUNCT_1:3;
[x0,(g . x0)] is set by TARSKI:1;
then reconsider z0 = [x0,(g . x0)] as Point of [:E,F:] by A14, PRVECT_3:18;
A15: ( 0 < r / 2 & r / 2 < r ) by A12, XREAL_1:215, XREAL_1:216;
consider q being Real such that
A16: ( 0 < q & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < q holds
||.((g /. x1) - (g /. x0)).|| < r / 2 ) ) by A1, A12, NFCONT_1:19, XREAL_1:215;
set pq = min (q,(r / 2));
A17: ( 0 < min (q,(r / 2)) & min (q,(r / 2)) <= q & min (q,(r / 2)) <= r / 2 ) by A15, A16, XXREAL_0:15, XXREAL_0:17;
take min (q,(r / 2)) ; :: thesis:
thus 0 < min (q,(r / 2)) by A15, A16, XXREAL_0:15; :: thesis:
thus for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < min (q,(r / 2)) holds
||.((H /. x1) - (H /. x0)).|| < r :: thesis:

let x1 be Point of E; :: thesis:
assume A18: ( x1 in S & ||.(x1 - x0).|| < min (q,(r / 2)) ) ; :: thesis:
then ||.(x1 - x0).|| < q by A17, XXREAL_0:2;
then A21: ||.((g /. x1) - (g /. x0)).|| < r / 2 by A16, A18;
A23: g . x1 in rng g by A2, A18, FUNCT_1:3;
[x1,(g . x1)] is set by TARSKI:1;
then reconsider z1 = [x1,(g . x1)] as Point of [:E,F:] by A23, PRVECT_3:18;
A24: z1 = [x1,(g /. x1)] by A2, A18, PARTFUN1:def 6;
z0 = [x0,(g /. x0)] by A2, A12, PARTFUN1:def 6;
then - z0 = [(- x0),(- (g /. x0))] by PRVECT_3:18;
then z1 - z0 = [(x1 - x0),((g /. x1) - (g /. x0))] by A24, PRVECT_3:18;
then A26: ||.(z1 - z0).|| = sqrt ((||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2)) by NDIFF_8:1;
||.(x1 - x0).|| < r / 2 by A17, A18, XXREAL_0:2;
then A27: ||.(x1 - x0).|| ^2 < (r / 2) ^2 by SQUARE_1:16;
||.((g /. x1) - (g /. x0)).|| ^2 <= (r / 2) ^2 by A21, SQUARE_1:15;
then A29: (||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) <= ((r ^2) / 4) + ((r ^2) / 4) by A27, XREAL_1:7;
(r ^2) / 2 < r ^2 by A12, XREAL_1:129, XREAL_1:216;
then (||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) < r ^2 by A29, XXREAL_0:2;
then A31: sqrt ((||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2)) < sqrt (r ^2) by SQUARE_1:27;
A32: H /. x1 = H . x1 by A7, A18, PARTFUN1:def 6
.= z1 by A11, A18 ;
H /. x0 = H . x0 by A7, A12, PARTFUN1:def 6
.= z0 by A11, A12 ;
hence ||.((H /. x1) - (H /. x0)).|| < r by A12, A26, A31, A32, SQUARE_1:22; :: thesis:

end;