let E be RealNormSpace; for G, F being non trivial RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for c being Point of G
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let G, F be non trivial RealBanachSpace; for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for c being Point of G
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let Z be Subset of [:E,F:]; for f being PartFunc of [:E,F:],G
for c being Point of G
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let f be PartFunc of [:E,F:],G; for c being Point of G
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let c be Point of G; for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let A be Subset of E; for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let B be Subset of F; for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
let g be PartFunc of E,F; ( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) implies ( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) ) )
assume A1:
( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) )
; ( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
then A2:
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
by NDIFF_7:52;
A3:
for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
( g is_differentiable_in x & diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
proof
let a be
Point of
E;
for z being Point of [:E,F:] st a in A & z = [a,(g . a)] holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )let z be
Point of
[:E,F:];
( a in A & z = [a,(g . a)] implies ( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
assume A4:
(
a in A &
z = [a,(g . a)] )
;
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
then A5:
g . a in rng g
by A1, FUNCT_1:def 3;
then reconsider b =
g . a as
Point of
F ;
A6:
f . (
a,
b)
= c
by A1, A4;
z in [:A,B:]
by A1, A4, A5, ZFMISC_1:87;
then A9:
f is_differentiable_in z
by A1, NDIFF_1:31;
A10:
g | A is_continuous_in a
by A1, A4, NFCONT_1:def 7;
A11:
g | A = g
by A1, RELAT_1:68;
partdiff`2 (
f,
z) is
invertible
by A1, A4;
hence
(
g is_differentiable_in a &
diff (
g,
a)
= - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
by A1, A4, A6, A9, A10, A11, Th45;
verum
end;
for x being Point of E st x in A holds
g is_differentiable_in x
hence A15:
g is_differentiable_on A
by A1, NDIFF_1:31; ( g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
then A16:
dom (g `| A) = A
by NDIFF_1:def 9;
consider xg being PartFunc of E,[:E,F:] such that
A17:
( dom xg = A & ( for x being Point of E st x in A holds
xg . x = [x,(g . x)] ) )
and
A18:
xg is_continuous_on A
by A1, LmTh471;
consider BL being BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (E,F)) such that
A19:
( BL is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds BL . (u,v) = v * u ) )
by LOPBAN13:29;
consider I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)) such that
A20:
( dom I = InvertibleOperators (F,G) & rng I = InvertibleOperators (G,F) & I is one-to-one & I is_continuous_on InvertibleOperators (F,G) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (G,F) & rng J = InvertibleOperators (F,G) & J is_continuous_on InvertibleOperators (G,F) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st u in InvertibleOperators (F,G) holds
I . u = Inv u ) )
by LOPBAN13:25;
A21:
dom (f `partial`1| Z) = Z
by A2, NDIFF_7:def 10;
A22:
dom (f `partial`2| Z) = Z
by A2, NDIFF_7:def 11;
A23:
for x being Point of E st x in A holds
(g `| A) /. x = - (BL /. [(((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)])
proof
let x be
Point of
E;
( x in A implies (g `| A) /. x = - (BL /. [(((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)]) )
assume A24:
x in A
;
(g `| A) /. x = - (BL /. [(((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)])
then A25:
(g `| A) /. x = diff (
g,
x)
by A15, NDIFF_1:def 9;
xg /. x =
xg . x
by A17, A24, PARTFUN1:def 6
.=
[x,(g . x)]
by A17, A24
;
then
partdiff`2 (
f,
(xg /. x)) is
invertible
by A1, A24;
then
partdiff`2 (
f,
(xg /. x))
in InvertibleOperators (
F,
G)
;
then A27:
I . (partdiff`2 (f,(xg /. x))) = Inv (partdiff`2 (f,(xg /. x)))
by A20;
[(partdiff`1 (f,(xg /. x))),(I . (partdiff`2 (f,(xg /. x))))] is
set
by TARSKI:1;
then
[(partdiff`1 (f,(xg /. x))),(I . (partdiff`2 (f,(xg /. x))))] is
Point of
[:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]
by A27, PRVECT_3:18;
then
[(partdiff`1 (f,(xg /. x))),(I . (partdiff`2 (f,(xg /. x))))] in the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]
;
then A28:
[(partdiff`1 (f,(xg /. x))),(I . (partdiff`2 (f,(xg /. x))))] in dom BL
by FUNCT_2:def 1;
A29:
(Inv (partdiff`2 (f,(xg /. x)))) * (partdiff`1 (f,(xg /. x))) =
BL . (
(partdiff`1 (f,(xg /. x))),
(I . (partdiff`2 (f,(xg /. x)))))
by A19, A27
.=
BL /. [(partdiff`1 (f,(xg /. x))),(I . (partdiff`2 (f,(xg /. x))))]
by A28, PARTFUN1:def 6
;
A30:
g . x in rng g
by A1, A24, FUNCT_1:def 3;
then reconsider y =
g . x as
Point of
F ;
reconsider z =
[x,y] as
Point of
[:E,F:] ;
A33:
(
z = xg . x &
xg . x = xg /. x )
by A17, A24, PARTFUN1:def 6;
A34:
z in [:A,B:]
by A1, A24, A30, ZFMISC_1:87;
A35:
((f `partial`1| Z) * xg) . x =
(f `partial`1| Z) . (xg . x)
by A17, A24, FUNCT_1:13
.=
(f `partial`1| Z) /. (xg . x)
by A1, A21, A33, A34, PARTFUN1:def 6
.=
partdiff`1 (
f,
(xg /. x))
by A1, A2, A33, A34, NDIFF_7:def 10
;
((I * (f `partial`2| Z)) * xg) . x =
(I * (f `partial`2| Z)) . (xg . x)
by A17, A24, FUNCT_1:13
.=
I . ((f `partial`2| Z) . (xg . x))
by A1, A22, A33, A34, FUNCT_1:13
.=
I . ((f `partial`2| Z) /. (xg . x))
by A1, A22, A33, A34, PARTFUN1:def 6
.=
I . (partdiff`2 (f,(xg /. x)))
by A1, A2, A33, A34, NDIFF_7:def 11
;
hence
(g `| A) /. x = - (BL /. [(((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)])
by A3, A24, A25, A29, A33, A35;
verum
end;
A39:
for x being Point of E st x in A holds
( x in dom ((f `partial`1| Z) * xg) & (f `partial`1| Z) * xg is_continuous_in x )
proof
let x be
Point of
E;
( x in A implies ( x in dom ((f `partial`1| Z) * xg) & (f `partial`1| Z) * xg is_continuous_in x ) )
assume A40:
x in A
;
( x in dom ((f `partial`1| Z) * xg) & (f `partial`1| Z) * xg is_continuous_in x )
then A41:
g . x in rng g
by A1, FUNCT_1:def 3;
[x,(g . x)] is
set
by TARSKI:1;
then reconsider z =
[x,(g . x)] as
Point of
[:E,F:] by A41, PRVECT_3:18;
A44:
z in [:A,B:]
by A1, A40, A41, ZFMISC_1:87;
A46:
(
xg . x = [x,(g . x)] &
xg . x = xg /. x )
by A17, A40, PARTFUN1:def 6;
hence A47:
x in dom ((f `partial`1| Z) * xg)
by A1, A17, A40, A21, A44, FUNCT_1:11;
(f `partial`1| Z) * xg is_continuous_in x
xg | A is_continuous_in x
by A18, A40, NFCONT_1:def 7;
then A48:
xg is_continuous_in x
by A17, RELAT_1:69;
(f `partial`1| Z) | Z is_continuous_in xg /. x
by A1, A2, A44, A46, NFCONT_1:def 7;
then
f `partial`1| Z is_continuous_in xg /. x
by A21, RELAT_1:69;
hence
(f `partial`1| Z) * xg is_continuous_in x
by A47, A48, NFCONT112;
verum
end;
A49:
for x being Point of E st x in A holds
( x in dom ((I * (f `partial`2| Z)) * xg) & (I * (f `partial`2| Z)) * xg is_continuous_in x )
proof
let x be
Point of
E;
( x in A implies ( x in dom ((I * (f `partial`2| Z)) * xg) & (I * (f `partial`2| Z)) * xg is_continuous_in x ) )
assume A50:
x in A
;
( x in dom ((I * (f `partial`2| Z)) * xg) & (I * (f `partial`2| Z)) * xg is_continuous_in x )
then A51:
g . x in rng g
by A1, FUNCT_1:def 3;
[x,(g . x)] is
set
by TARSKI:1;
then reconsider z =
[x,(g . x)] as
Point of
[:E,F:] by A51, PRVECT_3:18;
A54:
z in [:A,B:]
by A1, A50, A51, ZFMISC_1:87;
A56:
(
xg . x = [x,(g . x)] &
xg . x = xg /. x )
by A17, A50, PARTFUN1:def 6;
xg | A is_continuous_in x
by A18, A50, NFCONT_1:def 7;
then A58:
xg is_continuous_in x
by A17, RELAT_1:69;
(f `partial`2| Z) | Z is_continuous_in xg /. x
by A1, A2, A54, A56, NFCONT_1:def 7;
then A61:
f `partial`2| Z is_continuous_in xg /. x
by A22, RELAT_1:69;
A62:
partdiff`2 (
f,
(xg /. x)) is
invertible
by A1, A50, A56;
then A63:
partdiff`2 (
f,
(xg /. x))
in InvertibleOperators (
F,
G)
;
A64:
partdiff`2 (
f,
(xg /. x))
in dom I
by A20, A62;
A65:
(f `partial`2| Z) /. (xg /. x) = partdiff`2 (
f,
(xg /. x))
by A1, A2, A54, A56, NDIFF_7:def 11;
then
(f `partial`2| Z) . (xg /. x) in dom I
by A1, A22, A54, A56, A64, PARTFUN1:def 6;
then A68:
xg /. x in dom (I * (f `partial`2| Z))
by A1, A22, A54, A56, FUNCT_1:11;
hence A70:
x in dom ((I * (f `partial`2| Z)) * xg)
by A17, A50, A56, FUNCT_1:11;
(I * (f `partial`2| Z)) * xg is_continuous_in x
I | (InvertibleOperators (F,G)) is_continuous_in (f `partial`2| Z) /. (xg /. x)
by A20, A63, A65, NFCONT_1:def 7;
then
I is_continuous_in (f `partial`2| Z) /. (xg /. x)
by A20, RELAT_1:69;
then
I * (f `partial`2| Z) is_continuous_in xg /. x
by A61, A68, NFCONT112;
hence
(I * (f `partial`2| Z)) * xg is_continuous_in x
by A58, A70, NFCONT112;
verum
end;
for x being object st x in A holds
x in dom ((f `partial`1| Z) * xg)
by A39;
then A72:
A c= dom ((f `partial`1| Z) * xg)
by TARSKI:def 3;
for x being object st x in A holds
x in dom ((I * (f `partial`2| Z)) * xg)
by A49;
then A74:
A c= dom ((I * (f `partial`2| Z)) * xg)
by TARSKI:def 3;
A75:
for x being Point of E st x in A holds
(f `partial`1| Z) * xg is_continuous_in x
by A39;
for x being Point of E st x in A holds
(I * (f `partial`2| Z)) * xg is_continuous_in x
by A49;
then consider H being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) such that
A77:
( dom H = A & ( for x being Point of E st x in A holds
H . x = BL . ((((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)) ) & H is_continuous_on A )
by A19, A72, A74, A75, LmTh47;
A78:
for x0 being Point of E st x0 in A holds
BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)]
proof
let x0 be
Point of
E;
( x0 in A implies BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] )
assume
x0 in A
;
BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)]
then A82:
(
((f `partial`1| Z) * xg) . x0 in rng ((f `partial`1| Z) * xg) &
((I * (f `partial`2| Z)) * xg) . x0 in rng ((I * (f `partial`2| Z)) * xg) )
by A39, A49, FUNCT_1:3;
[(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] is
set
by TARSKI:1;
then
[(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] is
Point of
[:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]
by A82, PRVECT_3:18;
then
[(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] in the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]
;
then
[(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] in dom BL
by FUNCT_2:def 1;
hence
BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)]
by PARTFUN1:def 6;
verum
end;
for x0 being Point of E st x0 in A holds
(g `| A) | A is_continuous_in x0
proof
let x0 be
Point of
E;
( x0 in A implies (g `| A) | A is_continuous_in x0 )
assume A83:
x0 in A
;
(g `| A) | A is_continuous_in x0
then A85:
x0 in dom ((g `| A) | A)
by A16, RELAT_1:69;
set F =
(g `| A) | A;
for
r being
Real st
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1 being
Point of
E st
x1 in dom ((g `| A) | A) &
||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r ) )
proof
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r ) ) )
assume
0 < r
;
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r ) )
then consider s being
Real such that A88:
(
0 < s & ( for
x1 being
Point of
E st
x1 in A &
||.(x1 - x0).|| < s holds
||.((H /. x1) - (H /. x0)).|| < r ) )
by A77, A83, NFCONT_1:19;
take
s
;
( 0 < s & ( for x1 being Point of E st x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r ) )
thus
0 < s
by A88;
for x1 being Point of E st x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r
let x1 be
Point of
E;
( x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s implies ||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r )
assume A89:
(
x1 in dom ((g `| A) | A) &
||.(x1 - x0).|| < s )
;
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r
then A90:
x1 in A
by A16, RELAT_1:69;
then A91:
||.((H /. x1) - (H /. x0)).|| < r
by A88, A89;
A92:
H /. x1 =
H . x1
by A77, A90, PARTFUN1:def 6
.=
BL . (
(((f `partial`1| Z) * xg) . x1),
(((I * (f `partial`2| Z)) * xg) . x1))
by A77, A90
.=
BL /. [(((f `partial`1| Z) * xg) . x1),(((I * (f `partial`2| Z)) * xg) . x1)]
by A78, A90
;
A93:
((g `| A) | A) /. x1 =
(g `| A) /. x1
by A16, RELAT_1:69
.=
- (H /. x1)
by A23, A90, A92
;
A94:
H /. x0 =
H . x0
by A77, A83, PARTFUN1:def 6
.=
BL . (
(((f `partial`1| Z) * xg) . x0),
(((I * (f `partial`2| Z)) * xg) . x0))
by A77, A83
.=
BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)]
by A78, A83
;
((g `| A) | A) /. x0 =
(g `| A) /. x0
by A16, RELAT_1:69
.=
- (H /. x0)
by A23, A83, A94
;
then (((g `| A) | A) /. x1) - (((g `| A) | A) /. x0) =
(- (H /. x1)) + (H /. x0)
by A93, RLVECT_1:17
.=
- ((H /. x1) - (H /. x0))
by RLVECT_1:33
;
hence
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r
by A91, NORMSP_1:2;
verum
end;
hence
(g `| A) | A is_continuous_in x0
by A85, NFCONT_1:7;
verum
end;
hence
g `| A is_continuous_on A
by A16, NFCONT_1:def 7; for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z)))
thus
for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z)))
by A3; verum