let E, G be RealNormSpace; for F being RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let F be RealBanachSpace; for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let Z be Subset of [:E,F:]; for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let f be PartFunc of [:E,F:],G; for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let a be Point of E; for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let b be Point of F; for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let c be Point of G; for z being Point of [:E,F:] st Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
let z be Point of [:E,F:]; ( Z is open & dom f = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & f `partial`2| Z is_continuous_on Z & z = [a,b] & z in Z & f . (a,b) = c & partdiff`2 (f,z) is one-to-one & (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F implies ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) )
assume that
A1:
Z is open
and
A2:
dom f = Z
and
A3:
f is_continuous_on Z
and
A4:
f is_partial_differentiable_on`2 Z
and
A5:
f `partial`2| Z is_continuous_on Z
and
A6:
( z = [a,b] & z in Z )
and
A7:
f . (a,b) = c
and
A8:
partdiff`2 (f,z) is one-to-one
and
A9:
(partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F
; ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r1) & dom g = Ball (a,r1) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
consider QQ being Lipschitzian LinearOperator of G,F such that
A10:
QQ = (partdiff`2 (f,z)) "
by A9;
reconsider Q = QQ as Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) by LOPBAN_1:def 9;
set BLQ = ||.Q.||;
reconsider z1 = [a,(0. F)] as Point of [:E,F:] ;
reconsider e0b = [(0. E),b] as Point of [:E,F:] ;
A11: - e0b =
[(- (0. E)),(- b)]
by PRVECT_3:18
.=
[(0. E),(- b)]
by RLVECT_1:12
;
deffunc H1( Point of [:E,F:]) -> Element of the carrier of [:E,F:] = (1 * $1) + (- e0b);
consider H being Function of the carrier of [:E,F:], the carrier of [:E,F:] such that
A12:
for p being Point of [:E,F:] holds H . p = H1(p)
from FUNCT_2:sch 4();
A13:
for x being Point of E
for y being Point of F holds H . (x,y) = [x,(y - b)]
proof
let x be
Point of
E;
for y being Point of F holds H . (x,y) = [x,(y - b)]let y be
Point of
F;
H . (x,y) = [x,(y - b)]
reconsider p =
[x,y] as
Point of
[:E,F:] ;
A14: 1
* p =
[(1 * x),(1 * y)]
by PRVECT_3:18
.=
[x,(1 * y)]
by RLVECT_1:def 8
.=
[x,y]
by RLVECT_1:def 8
;
thus H . (
x,
y) =
(1 * p) + (- e0b)
by A12
.=
[(x + (0. E)),(y + (- b))]
by A11, A14, PRVECT_3:18
.=
[x,(y - b)]
by RLVECT_1:def 4
;
verum
end;
A15:
dom H = the carrier of [:E,F:]
by FUNCT_2:def 1;
deffunc H2( Point of [:E,F:]) -> Element of the carrier of [:E,F:] = (1 * $1) + e0b;
consider K being Function of the carrier of [:E,F:], the carrier of [:E,F:] such that
A16:
for p being Point of [:E,F:] holds K . p = H2(p)
from FUNCT_2:sch 4();
A17:
dom K = the carrier of [:E,F:]
by FUNCT_2:def 1;
for p being Point of [:E,F:] holds (K * H) . p = p
then A18:
K * H = id the carrier of [:E,F:]
by FUNCT_2:124;
then A19:
( H is one-to-one & K is onto )
by FUNCT_2:23;
for p being Point of [:E,F:] holds (H * K) . p = p
then
H * K = id the carrier of [:E,F:]
by FUNCT_2:124;
then
( K is one-to-one & H is onto )
by FUNCT_2:23;
then
rng H = the carrier of [:E,F:]
by FUNCT_2:def 3;
then A20:
K = H "
by A18, FUNCT_2:23, FUNCT_2:30;
reconsider Z1 = H .: Z as Subset of [:E,F:] ;
A21:
for x being Point of E
for y being Point of F holds
( [x,(y + b)] in Z iff [x,y] in Z1 )
proof
let x be
Point of
E;
for y being Point of F holds
( [x,(y + b)] in Z iff [x,y] in Z1 )let y be
Point of
F;
( [x,(y + b)] in Z iff [x,y] in Z1 )
hereby ( [x,y] in Z1 implies [x,(y + b)] in Z )
assume A22:
[x,(y + b)] in Z
;
[x,y] in Z1reconsider q =
[x,(y + b)] as
Point of
[:E,F:] ;
q in the
carrier of
[:E,F:]
;
then A23:
[x,(y + b)] in dom H
by FUNCT_2:def 1;
H . [x,(y + b)] =
H . (
x,
(y + b))
.=
[x,((y + b) - b)]
by A13
.=
[x,(y + (b - b))]
by RLVECT_1:28
.=
[x,(y + (0. F))]
by RLVECT_1:15
.=
[x,y]
by RLVECT_1:def 4
;
hence
[x,y] in Z1
by A22, A23, FUNCT_1:def 6;
verum
end;
assume
[x,y] in Z1
;
[x,(y + b)] in Z
then consider s being
object such that A24:
(
s in dom H &
s in Z &
[x,y] = H . s )
by FUNCT_1:def 6;
consider x1 being
Point of
E,
y1 being
Point of
F such that A25:
s = [x1,y1]
by A24, PRVECT_3:18;
A26:
H . [x1,y1] =
H . (
x1,
y1)
.=
[x1,(y1 - b)]
by A13
;
then
(
x = x1 &
y = y1 - b )
by A24, A25, XTUPLE_0:1;
then y + b =
y1 - (b - b)
by RLVECT_1:29
.=
y1 - (0. F)
by RLVECT_1:5
.=
y1
by RLVECT_1:13
;
hence
[x,(y + b)] in Z
by A24, A25, A26, XTUPLE_0:1;
verum
end;
reconsider e0b = [(0. E),b] as Point of [:E,F:] ;
A27:
for p being object holds
( p in Z1 iff p in { (y - e0b) where y is Point of [:E,F:] : y in Z } )
proof
let p be
object ;
( p in Z1 iff p in { (y - e0b) where y is Point of [:E,F:] : y in Z } )
A28:
- e0b =
[(- (0. E)),(- b)]
by PRVECT_3:18
.=
[(0. E),(- b)]
by RLVECT_1:12
;
hereby ( p in { (y - e0b) where y is Point of [:E,F:] : y in Z } implies p in Z1 )
assume A29:
p in Z1
;
p in { (y - e0b) where y is Point of [:E,F:] : y in Z } then consider s being
Point of
E,
t being
Point of
F such that A30:
p = [s,t]
by PRVECT_3:18;
A31:
[s,(t + b)] in Z
by A21, A29, A30;
reconsider y =
[s,(t + b)] as
Point of
[:E,F:] ;
y - e0b =
[(s + (0. E)),((t + b) + (- b))]
by A28, PRVECT_3:18
.=
[s,((t + b) - b)]
by RLVECT_1:def 4
.=
[s,(t + (b - b))]
by RLVECT_1:28
.=
[s,(t + (0. F))]
by RLVECT_1:15
.=
p
by A30, RLVECT_1:def 4
;
hence
p in { (y - e0b) where y is Point of [:E,F:] : y in Z }
by A31;
verum
end;
assume
p in { (y - e0b) where y is Point of [:E,F:] : y in Z }
;
p in Z1
then consider y being
Point of
[:E,F:] such that A32:
(
p = y - e0b &
y in Z )
;
consider s being
Point of
E,
t being
Point of
F such that A33:
y = [s,t]
by PRVECT_3:18;
A34:
p =
[(s + (0. E)),(t + (- b))]
by A28, A32, A33, PRVECT_3:18
.=
[s,(t - b)]
by RLVECT_1:def 4
;
(t - b) + b =
t - (b - b)
by RLVECT_1:29
.=
t - (0. F)
by RLVECT_1:15
.=
t
by RLVECT_1:13
;
hence
p in Z1
by A21, A32, A33, A34;
verum
end;
then A35:
Z1 = { (y - e0b) where y is Point of [:E,F:] : y in Z }
by TARSKI:2;
A36:
Z1 is open
by A1, A27, OP2, TARSKI:2;
defpred S1[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = (f /. [x,(y + b)]) - c );
A37:
for p being object st p in Z1 holds
ex w being object st
( w in the carrier of G & S1[p,w] )
consider f1 being Function of Z1,G such that
A39:
for p being object st p in Z1 holds
S1[p,f1 . p]
from FUNCT_2:sch 1(A37);
A40:
rng f1 c= the carrier of G
;
A41:
dom f1 = Z1
by FUNCT_2:def 1;
then
f1 in PFuncs ( the carrier of [:E,F:], the carrier of G)
by A40, PARTFUN1:def 3;
then reconsider f1 = f1 as PartFunc of [:E,F:],G by PARTFUN1:46;
A42:
for x being Point of E
for y being Point of F st [x,y] in Z1 holds
f1 . (x,y) = (f /. [x,(y + b)]) - c
proof
let x be
Point of
E;
for y being Point of F st [x,y] in Z1 holds
f1 . (x,y) = (f /. [x,(y + b)]) - clet y be
Point of
F;
( [x,y] in Z1 implies f1 . (x,y) = (f /. [x,(y + b)]) - c )
assume
[x,y] in Z1
;
f1 . (x,y) = (f /. [x,(y + b)]) - c
then consider x0 being
Point of
E,
y0 being
Point of
F such that A43:
(
[x,y] = [x0,y0] &
f1 . [x,y] = (f /. [x0,(y0 + b)]) - c )
by A39;
(
x = x0 &
y = y0 )
by A43, XTUPLE_0:1;
hence
f1 . (
x,
y)
= (f /. [x,(y + b)]) - c
by A43;
verum
end;
defpred S2[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = Q . (f1 . (x,y)) );
A44:
for p being object st p in Z1 holds
ex w being object st
( w in the carrier of F & S2[p,w] )
proof
let p be
object ;
( p in Z1 implies ex w being object st
( w in the carrier of F & S2[p,w] ) )
assume A45:
p in Z1
;
ex w being object st
( w in the carrier of F & S2[p,w] )
then consider x being
Point of
E,
y being
Point of
F such that A46:
p = [x,y]
by PRVECT_3:18;
A47:
Q . (f1 /. [x,y]) is
Point of
F
;
[x,y] in dom f1
by A45, A46, FUNCT_2:def 1;
then
f1 /. [x,y] = f1 . (
x,
y)
by PARTFUN1:def 6;
hence
ex
w being
object st
(
w in the
carrier of
F &
S2[
p,
w] )
by A46, A47;
verum
end;
consider f2 being Function of Z1,F such that
A48:
for p being object st p in Z1 holds
S2[p,f2 . p]
from FUNCT_2:sch 1(A44);
A49:
rng f2 c= the carrier of F
;
A50:
dom f2 = Z1
by FUNCT_2:def 1;
then
f2 in PFuncs ( the carrier of [:E,F:], the carrier of F)
by A49, PARTFUN1:def 3;
then reconsider f2 = f2 as PartFunc of [:E,F:],F by PARTFUN1:46;
A51:
for x being Point of E
for y being Point of F st [x,y] in Z1 holds
f2 . (x,y) = Q . (f1 . (x,y))
proof
let x be
Point of
E;
for y being Point of F st [x,y] in Z1 holds
f2 . (x,y) = Q . (f1 . (x,y))let y be
Point of
F;
( [x,y] in Z1 implies f2 . (x,y) = Q . (f1 . (x,y)) )
assume
[x,y] in Z1
;
f2 . (x,y) = Q . (f1 . (x,y))
then consider x0 being
Point of
E,
y0 being
Point of
F such that A52:
(
[x,y] = [x0,y0] &
f2 . [x,y] = Q . (f1 . (x0,y0)) )
by A48;
thus
f2 . (
x,
y)
= Q . (f1 . (x,y))
by A52;
verum
end;
defpred S3[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = y - (f2 /. [x,y]) );
A53:
for p being object st p in Z1 holds
ex w being object st
( w in the carrier of F & S3[p,w] )
consider Fai being Function of Z1,F such that
A55:
for p being object st p in Z1 holds
S3[p,Fai . p]
from FUNCT_2:sch 1(A53);
A56:
rng Fai c= the carrier of F
;
A57:
dom Fai = Z1
by FUNCT_2:def 1;
then
Fai in PFuncs ( the carrier of [:E,F:], the carrier of F)
by A56, PARTFUN1:def 3;
then reconsider Fai = Fai as PartFunc of [:E,F:],F by PARTFUN1:46;
A58:
for x being Point of E
for y being Point of F st [x,y] in Z1 holds
Fai . (x,y) = y - (f2 /. [x,y])
proof
let x be
Point of
E;
for y being Point of F st [x,y] in Z1 holds
Fai . (x,y) = y - (f2 /. [x,y])let y be
Point of
F;
( [x,y] in Z1 implies Fai . (x,y) = y - (f2 /. [x,y]) )
assume
[x,y] in Z1
;
Fai . (x,y) = y - (f2 /. [x,y])
then consider x0 being
Point of
E,
y0 being
Point of
F such that A59:
(
[x,y] = [x0,y0] &
Fai . [x,y] = y0 - (f2 /. [x0,y0]) )
by A55;
thus
Fai . (
x,
y)
= y - (f2 /. [x,y])
by A59, XTUPLE_0:1;
verum
end;
A60:
for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) )
proof
let z0 be
Point of
[:E,F:];
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) )let r be
Real;
( z0 in Z1 & 0 < r implies ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) ) )
assume A61:
(
z0 in Z1 &
0 < r )
;
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) )
reconsider w0 =
z0 + e0b as
Point of
[:E,F:] ;
consider x0 being
Point of
E,
y0 being
Point of
F such that A62:
z0 = [x0,y0]
by PRVECT_3:18;
A63:
0 < 2
* (||.Q.|| + 1)
by XREAL_1:129;
consider ww0 being
Point of
[:E,F:] such that A64:
(
z0 = ww0 - e0b &
ww0 in Z )
by A35, A61;
w0 =
ww0 - (e0b - e0b)
by A64, RLVECT_1:29
.=
ww0 - (0. [:E,F:])
by RLVECT_1:15
.=
ww0
by RLVECT_1:13
;
then consider s being
Real such that A65:
(
0 < s & ( for
w1 being
Point of
[:E,F:] st
w1 in Z &
||.(w1 - w0).|| < s holds
||.((f /. w1) - (f /. w0)).|| < r / (2 * (||.Q.|| + 1)) ) )
by A3, A61, A63, A64, NFCONT_1:19, XREAL_1:139;
reconsider s1 =
min (
s,
(r / 2)) as
Real ;
A66:
0 < r / 2
by A61, XREAL_1:215;
A67:
(
s1 <= s &
s1 <= r / 2 )
by XXREAL_0:17;
take
s1
;
( 0 < s1 & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s1 holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) )
thus
0 < s1
by A65, A66, XXREAL_0:15;
for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s1 holds
||.((Fai /. z1) - (Fai /. z0)).|| < r
thus
for
z1 being
Point of
[:E,F:] st
z1 in Z1 &
||.(z1 - z0).|| < s1 holds
||.((Fai /. z1) - (Fai /. z0)).|| < r
verumproof
let z1 be
Point of
[:E,F:];
( z1 in Z1 & ||.(z1 - z0).|| < s1 implies ||.((Fai /. z1) - (Fai /. z0)).|| < r )
assume A68:
(
z1 in Z1 &
||.(z1 - z0).|| < s1 )
;
||.((Fai /. z1) - (Fai /. z0)).|| < r
reconsider w1 =
z1 + e0b as
Point of
[:E,F:] ;
consider x1 being
Point of
E,
y1 being
Point of
F such that A69:
z1 = [x1,y1]
by PRVECT_3:18;
consider ww1 being
Point of
[:E,F:] such that A70:
(
z1 = ww1 - e0b &
ww1 in Z )
by A35, A68;
A71:
w1 =
ww1 - (e0b - e0b)
by A70, RLVECT_1:29
.=
ww1 - (0. [:E,F:])
by RLVECT_1:15
.=
ww1
by RLVECT_1:13
;
w1 - w0 =
((z1 + e0b) - e0b) - z0
by RLVECT_1:27
.=
z1 - z0
by RLVECT_4:1
;
then A72:
||.(w1 - w0).|| < s
by A67, A68, XXREAL_0:2;
A73:
Fai /. z1 =
Fai . (
x1,
y1)
by A57, A68, A69, PARTFUN1:def 6
.=
y1 - (f2 /. [x1,y1])
by A58, A68, A69
;
Fai /. z0 =
Fai . (
x0,
y0)
by A57, A61, A62, PARTFUN1:def 6
.=
y0 - (f2 /. [x0,y0])
by A58, A61, A62
;
then (Fai /. z1) - (Fai /. z0) =
((y1 - (f2 /. [x1,y1])) - y0) + (f2 /. [x0,y0])
by A73, RLVECT_1:29
.=
(y1 - ((f2 /. [x1,y1]) + y0)) + (f2 /. [x0,y0])
by RLVECT_1:27
.=
((y1 - y0) - (f2 /. [x1,y1])) + (f2 /. [x0,y0])
by RLVECT_1:27
.=
(y1 - y0) - ((f2 /. [x1,y1]) - (f2 /. [x0,y0]))
by RLVECT_1:29
;
then A75:
||.((Fai /. z1) - (Fai /. z0)).|| <= ||.(y1 - y0).|| + ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).||
by NORMSP_1:3;
A76:
f2 /. [x1,y1] =
f2 . (
x1,
y1)
by A50, A68, A69, PARTFUN1:def 6
.=
Q . (f1 . (x1,y1))
by A51, A68, A69
;
A77:
f2 /. [x0,y0] =
f2 . (
x0,
y0)
by A50, A61, A62, PARTFUN1:def 6
.=
Q . (f1 . (x0,y0))
by A51, A61, A62
;
[x1,(y1 + b)] =
[(x1 + (0. E)),(y1 + b)]
by RLVECT_1:4
.=
w1
by A69, PRVECT_3:18
;
then A79:
f1 . (
x1,
y1)
= (f /. w1) - c
by A42, A68, A69;
[x0,(y0 + b)] =
[(x0 + (0. E)),(y0 + b)]
by RLVECT_1:4
.=
w0
by A62, PRVECT_3:18
;
then A81:
f1 . (
x0,
y0)
= (f /. w0) - c
by A42, A61, A62;
A82:
((f /. w1) - c) - ((f /. w0) - c) =
(((f /. w1) - c) - (f /. w0)) + c
by RLVECT_1:29
.=
((f /. w1) - (c + (f /. w0))) + c
by RLVECT_1:27
.=
(((f /. w1) - (f /. w0)) - c) + c
by RLVECT_1:27
.=
((f /. w1) - (f /. w0)) - (c - c)
by RLVECT_1:29
.=
((f /. w1) - (f /. w0)) - (0. G)
by RLVECT_1:15
.=
(f /. w1) - (f /. w0)
by RLVECT_1:13
;
A83:
QQ is
additive
;
A84:
(f2 /. [x1,y1]) - (f2 /. [x0,y0]) =
(Q . ((f /. w1) - c)) + ((- 1) * (Q . ((f /. w0) - c)))
by A76, A77, A79, A81, RLVECT_1:16
.=
(Q . ((f /. w1) - c)) + (Q . ((- 1) * ((f /. w0) - c)))
by LOPBAN_1:def 5
.=
Q . (((f /. w1) - c) + ((- 1) * ((f /. w0) - c)))
by A83
.=
Q . ((f /. w1) - (f /. w0))
by A82, RLVECT_1:16
;
||.Q.|| + 0 < ||.Q.|| + 1
by XREAL_1:8;
then A85:
||.Q.|| * ||.((f /. w1) - (f /. w0)).|| <= (||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).||
by XREAL_1:64;
||.(Q . ((f /. w1) - (f /. w0))).|| <= ||.Q.|| * ||.((f /. w1) - (f /. w0)).||
by LOPBAN_1:32;
then A86:
||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| <= (||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).||
by A84, A85, XXREAL_0:2;
- z0 = [(- x0),(- y0)]
by A62, PRVECT_3:18;
then
z1 - z0 = [(x1 - x0),(y1 - y0)]
by A69, PRVECT_3:18;
then
||.(y1 - y0).|| <= ||.(z1 - z0).||
by NORMSP35;
then
||.(y1 - y0).|| < s1
by A68, XXREAL_0:2;
then A88:
||.(y1 - y0).|| < r / 2
by A67, XXREAL_0:2;
(||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).|| < (||.Q.|| + 1) * (r / (2 * (||.Q.|| + 1)))
by A65, A70, A71, A72, XREAL_1:68;
then
||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < (||.Q.|| + 1) * (r / (2 * (||.Q.|| + 1)))
by A86, XXREAL_0:2;
then
||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < r / 2
by XCMPLX_1:92;
then
||.(y1 - y0).|| + ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < (r / 2) + (r / 2)
by A88, XREAL_1:8;
hence
||.((Fai /. z1) - (Fai /. z0)).|| < r
by A75, XXREAL_0:2;
verum
end;
end;
A89:
for w0 being Point of [:E,F:] st w0 in Z holds
f * (reproj2 w0) is_differentiable_in w0 `2
A90:
for w0 being Point of [:E,F:] st w0 in Z holds
ex N being Neighbourhood of w0 `2 st
( N c= dom (f * (reproj2 w0)) & ex R being RestFunc of F,G st
for w1 being Point of F st w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) )
A91:
for z0 being Point of [:E,F:] st z0 in Z1 holds
( Fai * (reproj2 z0) is_differentiable_in z0 `2 & ex L0, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 ) )
proof
let z0 be
Point of
[:E,F:];
( z0 in Z1 implies ( Fai * (reproj2 z0) is_differentiable_in z0 `2 & ex L0, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 ) ) )
assume A92:
z0 in Z1
;
( Fai * (reproj2 z0) is_differentiable_in z0 `2 & ex L0, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 ) )
reconsider w0 =
z0 + e0b as
Point of
[:E,F:] ;
consider x0 being
Point of
E,
y0 being
Point of
F such that A93:
z0 = [x0,y0]
by PRVECT_3:18;
consider ww0 being
Point of
[:E,F:] such that A94:
(
z0 = ww0 - e0b &
ww0 in Z )
by A35, A92;
A95:
w0 =
ww0 - (e0b - e0b)
by A94, RLVECT_1:29
.=
ww0 - (0. [:E,F:])
by RLVECT_1:15
.=
ww0
by RLVECT_1:13
;
then consider N being
Neighbourhood of
w0 `2 such that A96:
(
N c= dom (f * (reproj2 w0)) & ex
R being
RestFunc of
F,
G st
for
w1 being
Point of
F st
w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) )
by A90, A94;
consider R being
RestFunc of
F,
G such that A97:
for
w1 being
Point of
F st
w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2)))
by A96;
reconsider L0 =
Q * ((f `partial`2| Z) /. (z0 + e0b)) as
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) ;
id the
carrier of
F is
Lipschitzian LinearOperator of
F,
F
by LOPBAN_2:3;
then reconsider I =
id the
carrier of
F as
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;
reconsider L1 =
I - L0 as
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) ;
reconsider R0 =
Q * R as
RestFunc of
F,
F by NDIFF_2:9;
reconsider R1 =
(- 1) (#) R0 as
RestFunc of
F,
F by NDIFF_1:29;
A98:
w0 =
[(x0 + (0. E)),(y0 + b)]
by A93, PRVECT_3:18
.=
[x0,(y0 + b)]
by RLVECT_1:4
;
then A99:
(
w0 `1 = x0 &
w0 `2 = y0 + b )
;
A100:
(
z0 `1 = x0 &
z0 `2 = y0 )
by A93;
set N1 =
{ (z - b) where z is Point of F : z in N } ;
{ (z - b) where z is Point of F : z in N } is
Neighbourhood of
(y0 + b) - b
by A98, NEIB1;
then reconsider N1 =
{ (z - b) where z is Point of F : z in N } as
Neighbourhood of
y0 by RLVECT_4:1;
A101:
now for yy1 being object st yy1 in N1 holds
yy1 in dom (Fai * (reproj2 z0))let yy1 be
object ;
( yy1 in N1 implies yy1 in dom (Fai * (reproj2 z0)) )assume A102:
yy1 in N1
;
yy1 in dom (Fai * (reproj2 z0))then reconsider y1 =
yy1 as
Point of
F ;
A103:
(reproj2 z0) . y1 = [x0,y1]
by A100, NDIFF_7:def 2;
consider w being
Point of
F such that A104:
(
y1 = w - b &
w in N )
by A102;
(reproj2 w0) . w in dom f
by A96, A104, FUNCT_1:11;
then A105:
[(w0 `1),w] in dom f
by NDIFF_7:def 2;
reconsider x0w =
[x0,w] as
Point of
[:E,F:] ;
A106:
- e0b = [(- (0. E)),(- b)]
by PRVECT_3:18;
[x0,(w - b)] =
[(x0 - (0. E)),(w - b)]
by RLVECT_1:13
.=
x0w - e0b
by A106, PRVECT_3:18
;
then A107:
[x0,(w - b)] in Z1
by A2, A35, A98, A105;
dom (reproj2 z0) = the
carrier of
F
by FUNCT_2:def 1;
hence
yy1 in dom (Fai * (reproj2 z0))
by A57, A103, A104, A107, FUNCT_1:11;
verum end;
then A108:
N1 c= dom (Fai * (reproj2 z0))
by TARSKI:def 3;
A109:
now for y1 being Point of F st y1 in N1 holds
((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. (z0 `2)) = (L1 . (y1 - (z0 `2))) + (R1 /. (y1 - (z0 `2)))let y1 be
Point of
F;
( y1 in N1 implies ((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. (z0 `2)) = (L1 . (y1 - (z0 `2))) + (R1 /. (y1 - (z0 `2))) )assume A110:
y1 in N1
;
((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. (z0 `2)) = (L1 . (y1 - (z0 `2))) + (R1 /. (y1 - (z0 `2)))A111:
(reproj2 z0) . y1 = [x0,y1]
by A100, NDIFF_7:def 2;
consider w being
Point of
F such that A112:
(
y1 = w - b &
w in N )
by A110;
(reproj2 w0) . w in dom f
by A96, A112, FUNCT_1:11;
then A113:
[(w0 `1),w] in dom f
by NDIFF_7:def 2;
reconsider x0w =
[x0,w] as
Point of
[:E,F:] ;
A114:
- e0b = [(- (0. E)),(- b)]
by PRVECT_3:18;
[x0,(w - b)] =
[(x0 - (0. E)),(w - b)]
by RLVECT_1:13
.=
x0w - e0b
by A114, PRVECT_3:18
;
then A115:
[x0,(w - b)] in Z1
by A2, A35, A98, A113;
dom (reproj2 z0) = the
carrier of
F
by FUNCT_2:def 1;
then A116:
y1 in dom (Fai * (reproj2 z0))
by A57, A111, A112, A115, FUNCT_1:11;
A117:
(Fai * (reproj2 z0)) /. y1 =
(Fai * (reproj2 z0)) . y1
by A116, PARTFUN1:def 6
.=
Fai . (
x0,
y1)
by A111, A116, FUNCT_1:12
.=
y1 - (f2 /. [x0,y1])
by A58, A112, A115
;
A118:
f2 /. [x0,y1] =
f2 . (
x0,
y1)
by A50, A112, A115, PARTFUN1:def 6
.=
Q . (f1 . (x0,y1))
by A51, A112, A115
;
A119:
[x0,(y1 + b)] = [x0,w]
by A112, RLVECT_4:1;
A120:
[x0,w] = (reproj2 w0) . w
by A99, NDIFF_7:def 2;
A121:
(f * (reproj2 w0)) /. w =
(f * (reproj2 w0)) . w
by A96, A112, PARTFUN1:def 6
.=
f . [x0,(y1 + b)]
by A96, A112, A119, A120, FUNCT_1:12
.=
f /. [x0,(y1 + b)]
by A98, A113, A119, PARTFUN1:def 6
;
A122:
f1 . (
x0,
y1)
= ((f * (reproj2 w0)) /. w) - c
by A42, A112, A115, A121;
A123:
(reproj2 z0) . y0 = [x0,y0]
by A100, NDIFF_7:def 2;
A124:
y0 + b in N
by A98, NFCONT_1:4;
(reproj2 w0) . (y0 + b) in dom f
by A96, A124, FUNCT_1:11;
then A125:
[(w0 `1),(y0 + b)] in dom f
by NDIFF_7:def 2;
reconsider x0v =
[x0,(y0 + b)] as
Point of
[:E,F:] ;
dom (reproj2 z0) = the
carrier of
F
by FUNCT_2:def 1;
then A126:
y0 in dom (Fai * (reproj2 z0))
by A57, A92, A93, A123, FUNCT_1:11;
then A127:
(Fai * (reproj2 z0)) /. y0 =
(Fai * (reproj2 z0)) . y0
by PARTFUN1:def 6
.=
Fai . (
x0,
y0)
by A123, A126, FUNCT_1:12
.=
y0 - (f2 /. [x0,y0])
by A58, A92, A93
;
A128:
f2 /. [x0,y0] =
f2 . (
x0,
y0)
by A50, A92, A93, PARTFUN1:def 6
.=
Q . (f1 . (x0,y0))
by A51, A92, A93
;
A129:
[x0,(y0 + b)] = (reproj2 w0) . (y0 + b)
by A99, NDIFF_7:def 2;
A130:
(f * (reproj2 w0)) /. (y0 + b) =
(f * (reproj2 w0)) . (y0 + b)
by A96, A124, PARTFUN1:def 6
.=
f . [x0,(y0 + b)]
by A96, A124, A129, FUNCT_1:12
.=
f /. [x0,(y0 + b)]
by A98, A125, PARTFUN1:def 6
;
A131:
f1 . (
x0,
y0)
= ((f * (reproj2 w0)) /. (w0 `2)) - c
by A42, A92, A93, A98, A130;
A132:
f1 /. [x0,y1] = f1 . (
x0,
y1)
by A41, A112, A115, PARTFUN1:def 6;
A133:
f1 /. [x0,y0] = f1 . (
x0,
y0)
by A41, A92, A93, PARTFUN1:def 6;
A134:
QQ is
additive
;
A135:
(f2 /. [x0,y1]) - (f2 /. [x0,y0]) =
(Q . (f1 /. [x0,y1])) + ((- 1) * (Q . (f1 /. [x0,y0])))
by A118, A128, A132, A133, RLVECT_1:16
.=
(Q . (f1 /. [x0,y1])) + (Q . ((- 1) * (f1 /. [x0,y0])))
by LOPBAN_1:def 5
.=
Q . ((f1 /. [x0,y1]) + ((- 1) * (f1 /. [x0,y0])))
by A134
.=
Q . ((f1 /. [x0,y1]) - (f1 /. [x0,y0]))
by RLVECT_1:16
;
A136:
w - (w0 `2) = y1 - y0
by A98, A112, RLVECT_1:27;
(f1 /. [x0,y1]) - (f1 /. [x0,y0]) =
((((f * (reproj2 w0)) /. w) - c) - ((f * (reproj2 w0)) /. (w0 `2))) + c
by A122, A131, A132, A133, RLVECT_1:29
.=
(((f * (reproj2 w0)) /. w) - (c + ((f * (reproj2 w0)) /. (w0 `2)))) + c
by RLVECT_1:27
.=
((((f * (reproj2 w0)) /. w) - ((f * (reproj2 w0)) /. (w0 `2))) - c) + c
by RLVECT_1:27
.=
((f * (reproj2 w0)) /. w) - ((f * (reproj2 w0)) /. (w0 `2))
by RLVECT_4:1
.=
((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0)) + (R /. (y1 - y0))
by A97, A98, A112, A136
;
then A137:
(f2 /. [x0,y1]) - (f2 /. [x0,y0]) = (Q . ((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0))) + (Q . (R /. (y1 - y0)))
by A134, A135;
A138:
diff (
(f * (reproj2 w0)),
(y0 + b)) =
partdiff`2 (
f,
w0)
by A99, NDIFF_7:def 7
.=
(f `partial`2| Z) /. (z0 + e0b)
by A4, A94, A95, NDIFF_7:def 11
;
set Q1 =
modetrans (
Q,
G,
F);
set df1 =
modetrans (
(diff ((f * (reproj2 w0)),(y0 + b))),
F,
G);
A139:
(modetrans (Q,G,F)) * (modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) is
Lipschitzian LinearOperator of
F,
F
by LOPBAN_2:2;
A140:
Q . ((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0)) =
Q . ((modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) . (y1 - y0))
by LOPBAN_1:def 11
.=
(modetrans (Q,G,F)) . ((modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) . (y1 - y0))
by LOPBAN_1:def 11
.=
(Q * ((f `partial`2| Z) /. (z0 + e0b))) . (y1 - y0)
by A138, A139, LPB2Th4
;
R is
total
by NDIFF_1:def 5;
then A141:
dom R = the
carrier of
F
by PARTFUN1:def 2;
rng R c= the
carrier of
G
;
then
rng R c= dom Q
by FUNCT_2:def 1;
then A142:
dom (Q * R) = dom R
by RELAT_1:27;
A143:
dom ((- 1) (#) (QQ * R)) = the
carrier of
F
by A141, A142, VFUNCT_1:def 4;
A144:
Q . (R /. (y1 - y0)) =
Q . (R . (y1 - y0))
by A141, PARTFUN1:def 6
.=
(Q * R) . (y1 - y0)
by A141, FUNCT_1:13
.=
(QQ * R) /. (y1 - y0)
by A141, A142, PARTFUN1:def 6
;
((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. y0) =
((y1 - (f2 /. [x0,y1])) - y0) + (f2 /. [x0,y0])
by A117, A127, RLVECT_1:29
.=
(y1 - ((f2 /. [x0,y1]) + y0)) + (f2 /. [x0,y0])
by RLVECT_1:27
.=
((y1 - y0) - (f2 /. [x0,y1])) + (f2 /. [x0,y0])
by RLVECT_1:27
.=
(y1 - y0) - ((L0 . (y1 - y0)) + (R0 /. (y1 - y0)))
by A137, A140, A144, RLVECT_1:29
.=
((y1 - y0) - (L0 . (y1 - y0))) - (R0 /. (y1 - y0))
by RLVECT_1:27
.=
((y1 - y0) + (- (L0 . (y1 - y0)))) + ((- 1) * (R0 /. (y1 - y0)))
by RLVECT_1:16
.=
((I . (y1 - y0)) - (L0 . (y1 - y0))) + (((- 1) (#) R0) /. (y1 - y0))
by A143, VFUNCT_1:def 4
.=
(L1 . (y1 - y0)) + (R1 /. (y1 - y0))
by LOPBAN_1:40
;
hence
((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. (z0 `2)) = (L1 . (y1 - (z0 `2))) + (R1 /. (y1 - (z0 `2)))
by A93;
verum end;
hence A145:
Fai * (reproj2 z0) is_differentiable_in z0 `2
by A93, A101, NDIFF_1:def 6, TARSKI:def 3;
ex L0, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 )
take
L0
;
ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 )
take
I
;
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 )
thus
(
L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) &
I = id the
carrier of
F &
diff (
(Fai * (reproj2 z0)),
(z0 `2))
= I - L0 )
by A93, A108, A109, A145, NDIFF_1:def 7;
verum
end;
for z0 being Point of [:E,F:] st z0 in Z1 holds
Fai is_partial_differentiable_in`2 z0
by A91;
then A146:
Fai is_partial_differentiable_on`2 Z1
by FUNCT_2:def 1;
A147:
( dom (Fai `partial`2| Z1) = Z1 & ( for z being Point of [:E,F:] st z in Z1 holds
ex L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L ) ) )
proof
thus
dom (Fai `partial`2| Z1) = Z1
by A146, NDIFF_7:def 11;
for z being Point of [:E,F:] st z in Z1 holds
ex L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L )
let z be
Point of
[:E,F:];
( z in Z1 implies ex L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L ) )
assume A148:
z in Z1
;
ex L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L )
then consider L,
I being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) such that A149:
(
L = Q * ((f `partial`2| Z) /. (z + e0b)) &
I = id the
carrier of
F &
diff (
(Fai * (reproj2 z)),
(z `2))
= I - L )
by A91;
take
L
;
ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L )
take
I
;
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L )
thus
(
L = Q * ((f `partial`2| Z) /. (z + e0b)) &
I = id the
carrier of
F )
by A149;
(Fai `partial`2| Z1) /. z = I - L
thus (Fai `partial`2| Z1) /. z =
partdiff`2 (
Fai,
z)
by A146, A148, NDIFF_7:def 11
.=
I - L
by A149, NDIFF_7:def 7
;
verum
end;
set FG = Fai `partial`2| Z1;
A150:
for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) )
proof
let z0 be
Point of
[:E,F:];
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) )let r be
Real;
( z0 in Z1 & 0 < r implies ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) ) )
reconsider w0 =
z0 + e0b as
Point of
[:E,F:] ;
assume A151:
(
z0 in Z1 &
0 < r )
;
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) )
then consider ww0 being
Point of
[:E,F:] such that A152:
(
z0 = ww0 - e0b &
ww0 in Z )
by A35;
w0 =
ww0 - (e0b - e0b)
by A152, RLVECT_1:29
.=
ww0 - (0. [:E,F:])
by RLVECT_1:15
.=
ww0
by RLVECT_1:13
;
then consider s being
Real such that A153:
(
0 < s & ( for
w1 being
Point of
[:E,F:] st
w1 in Z &
||.(w1 - w0).|| < s holds
||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| < r / (||.Q.|| + 1) ) )
by A5, A151, A152, NFCONT_1:19, XREAL_1:139;
take
s
;
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) )
thus
0 < s
by A153;
for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r
thus
for
z1 being
Point of
[:E,F:] st
z1 in Z1 &
||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r
verumproof
let z1 be
Point of
[:E,F:];
( z1 in Z1 & ||.(z1 - z0).|| < s implies ||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r )
reconsider w1 =
z1 + e0b as
Point of
[:E,F:] ;
assume A154:
(
z1 in Z1 &
||.(z1 - z0).|| < s )
;
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r
then consider ww1 being
Point of
[:E,F:] such that A155:
(
z1 = ww1 - e0b &
ww1 in Z )
by A35;
A156:
w1 =
ww1 - (e0b - e0b)
by A155, RLVECT_1:29
.=
ww1 - (0. [:E,F:])
by RLVECT_1:15
.=
ww1
by RLVECT_1:13
;
A157:
w1 - w0 =
((z1 + e0b) - e0b) - z0
by RLVECT_1:27
.=
z1 - z0
by RLVECT_4:1
;
consider Lz0,
Iz0 being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) such that A158:
(
Lz0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) &
Iz0 = id the
carrier of
F &
(Fai `partial`2| Z1) /. z0 = Iz0 - Lz0 )
by A147, A151;
consider Lz1,
Iz1 being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) such that A159:
(
Lz1 = Q * ((f `partial`2| Z) /. (z1 + e0b)) &
Iz1 = id the
carrier of
F &
(Fai `partial`2| Z1) /. z1 = Iz1 - Lz1 )
by A147, A154;
((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0) =
((Iz1 - Lz1) - Iz0) + Lz0
by A158, A159, RLVECT_1:29
.=
(Iz1 - (Iz0 + Lz1)) + Lz0
by RLVECT_1:27
.=
((Iz1 - Iz0) - Lz1) + Lz0
by RLVECT_1:27
.=
(Iz1 - Iz0) - (Lz1 - Lz0)
by RLVECT_1:29
.=
(0. (R_NormSpace_of_BoundedLinearOperators (F,F))) - (Lz1 - Lz0)
by A158, A159, RLVECT_1:15
.=
- (Lz1 - Lz0)
by RLVECT_1:14
;
then A160:
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| = ||.(Lz1 - Lz0).||
by NORMSP_1:2;
||.Q.|| + 0 < ||.Q.|| + 1
by XREAL_1:8;
then A161:
||.Q.|| * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| <= (||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||
by XREAL_1:64;
A162:
Q * ((- 1) * ((f `partial`2| Z) /. w0)) =
(1 * Q) * ((- 1) * ((f `partial`2| Z) /. w0))
by RLVECT_1:def 8
.=
(1 * (- 1)) * (Q * ((f `partial`2| Z) /. w0))
by LPB2Th11
.=
- (Q * ((f `partial`2| Z) /. w0))
by RLVECT_1:16
;
A163:
(Q * ((f `partial`2| Z) /. w1)) - (Q * ((f `partial`2| Z) /. w0)) =
Q * (((f `partial`2| Z) /. w1) + ((- 1) * ((f `partial`2| Z) /. w0)))
by A162, LPB2Th9
.=
Q * (((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0))
by RLVECT_1:16
;
set Q1 =
modetrans (
Q,
G,
F);
set fp10 =
modetrans (
(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)),
F,
G);
A164:
(BoundedLinearOperatorsNorm (G,F)) . (modetrans (Q,G,F)) = ||.Q.||
by LOPBAN_1:def 11;
||.(Lz1 - Lz0).|| <= ((BoundedLinearOperatorsNorm (G,F)) . (modetrans (Q,G,F))) * ((BoundedLinearOperatorsNorm (F,G)) . (modetrans ((((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)),F,G)))
by A158, A159, A163, LOPBAN_2:2;
then
||.(Lz1 - Lz0).|| <= ||.Q.|| * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||
by A164, LOPBAN_1:def 11;
then A165:
||.(Lz1 - Lz0).|| <= (||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||
by A161, XXREAL_0:2;
(||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| < (||.Q.|| + 1) * (r / (||.Q.|| + 1))
by A153, A154, A155, A156, A157, XREAL_1:68;
then
||.(Lz1 - Lz0).|| < (||.Q.|| + 1) * (r / (||.Q.|| + 1))
by A165, XXREAL_0:2;
hence
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r
by A160, XCMPLX_1:87;
verum
end;
end;
A166:
[a,((0. F) + b)] in Z
by A6, RLVECT_1:def 4;
then A167:
[a,(0. F)] in Z1
by A21;
A169:
Fai . (a,(0. F)) = (0. F) - (f2 /. [a,(0. F)])
by A21, A58, A166;
A168:
Fai . (a,(0. F)) = 0. F
proof
f2 /. [a,(0. F)] =
f2 . (
a,
(0. F))
by A21, A50, A166, PARTFUN1:def 6
.=
Q . (f1 . (a,(0. F)))
by A21, A51, A166
.=
Q . ((f /. [a,((0. F) + b)]) - c)
by A21, A42, A166
.=
Q . ((f /. [a,b]) - c)
by RLVECT_1:def 4
.=
Q . (c - c)
by A2, A6, A7, PARTFUN1:def 6
.=
Q . (0. G)
by RLVECT_1:15
.=
0. F
by LOPBAN_7:3
;
hence
Fai . (
a,
(0. F))
= 0. F
by A169, RLVECT_1:15;
verum
end;
reconsider a0F = [a,(0. F)] as Point of [:E,F:] ;
consider r10 being Real such that
A170:
( 0 < r10 & ( for s being Point of [:E,F:] st s in Z1 & ||.(s - a0F).|| < r10 holds
||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < 1 / 4 ) )
by A21, A150, A166;
consider r11 being Real such that
A171:
( 0 < r11 & Ball (a0F,r11) c= Z1 )
by A21, A36, A166, NORMSP27;
reconsider r12 = min (r10,r11) as Real ;
A173:
( r12 <= r11 & r12 <= r10 )
by XXREAL_0:17;
then A174:
Ball (a0F,r12) c= Ball (a0F,r11)
by LMBALL1;
0 < r12
by A170, A171, XXREAL_0:15;
then consider r1 being Real such that
A175:
( 0 < r1 & r1 < r12 & [:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Ball (a0F,r12) )
by NORMSP31;
[:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Ball (a0F,r11)
by A174, A175, XBOOLE_1:1;
then A176:
[:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Z1
by A171, XBOOLE_1:1;
A177:
for x being Point of [:E,F:] st x in Z1 holds
(Fai `partial`2| Z1) /. x = diff ((Fai * (reproj2 x)),(x `2))
A179:
a in Ball (a,r1)
by A175, LMBALL2;
0. F in Ball ((0. F),r1)
by A175, LMBALL2;
then A181:
[a,(0. F)] in [:(Ball (a,r1)),(Ball ((0. F),r1)):]
by A179, ZFMISC_1:87;
reconsider a0F = [a,(0. F)] as Point of [:E,F:] ;
consider La0f, Ia0f being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A182:
( La0f = Q * ((f `partial`2| Z) /. (a0F + e0b)) & Ia0f = id the carrier of F & (Fai `partial`2| Z1) /. a0F = Ia0f - La0f )
by A147, A176, A181;
partdiff`2 (f,z) is Lipschitzian LinearOperator of F,G
by LOPBAN_1:def 9;
then A183:
dom (partdiff`2 (f,z)) = the carrier of F
by FUNCT_2:def 1;
A184:
Q = modetrans (((partdiff`2 (f,z)) "),G,F)
by A10, LOPBAN_1:def 11;
A185:
partdiff`2 (f,z) = modetrans ((partdiff`2 (f,z)),F,G)
by LOPBAN_1:def 11;
a0F + e0b =
[(a + (0. E)),((0. F) + b)]
by PRVECT_3:18
.=
[a,((0. F) + b)]
by RLVECT_1:4
.=
z
by A6, RLVECT_1:4
;
then A186: La0f =
Q * (partdiff`2 (f,z))
by A4, A6, A182, NDIFF_7:def 11
.=
Ia0f
by A8, A10, A182, A183, A184, A185, FUNCT_1:39
;
A187:
(Fai `partial`2| Z1) /. [a,(0. F)] = 0. (R_NormSpace_of_BoundedLinearOperators (F,F))
by A182, A186, RLVECT_1:15;
A188:
for x being Point of E
for y being Point of F st x in Ball (a,r1) & y in Ball ((0. F),r1) holds
||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4
proof
let x be
Point of
E;
for y being Point of F st x in Ball (a,r1) & y in Ball ((0. F),r1) holds
||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4let y be
Point of
F;
( x in Ball (a,r1) & y in Ball ((0. F),r1) implies ||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4 )
assume
(
x in Ball (
a,
r1) &
y in Ball (
(0. F),
r1) )
;
||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4
then A190:
[x,y] in [:(Ball (a,r1)),(Ball ((0. F),r1)):]
by ZFMISC_1:87;
reconsider s =
[x,y] as
Point of
[:E,F:] ;
s in Ball (
a0F,
r12)
by A175, A190;
then
ex
q being
Element of
[:E,F:] st
(
s = q &
||.(a0F - q).|| < r12 )
;
then
||.(s - a0F).|| < r12
by NORMSP_1:7;
then
||.(s - a0F).|| < r10
by A173, XXREAL_0:2;
then
||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < 1
/ 4
by A170, A176, A190;
hence
||.((Fai `partial`2| Z1) /. [x,y]).|| < 1
/ 4
by A187, RLVECT_1:13;
verum
end;
reconsider r2 = r1 / 2 as Real ;
( 0 < 1 / 2 & 0 < r1 / 2 )
by A175, XREAL_1:215;
then consider ar10 being Real such that
A191:
( 0 < ar10 & ( for s being Point of [:E,F:] st s in Z1 & ||.(s - a0F).|| < ar10 holds
||.((Fai /. s) - (Fai /. a0F)).|| < (1 / 2) * r2 ) )
by A60, A167, XREAL_1:129;
consider ar12 being Real such that
A192:
( 0 < ar12 & ar12 < ar10 & [:(Ball (a,ar12)),(Ball ((0. F),ar12)):] c= Ball (a0F,ar10) )
by A191, NORMSP31;
reconsider ar11 = min (ar10,ar12) as Real ;
A193:
0 < ar11
by A192, XXREAL_0:21;
( ar11 <= ar10 & ar11 <= ar12 )
by XXREAL_0:17;
then A195:
Ball (a,ar11) c= Ball (a,ar12)
by LMBALL1;
reconsider ar1 = min (ar11,r1) as Real ;
A196:
0 < ar1
by A175, A193, XXREAL_0:21;
A197:
( ar1 <= ar11 & ar1 <= r1 )
by XXREAL_0:17;
then A198:
Ball (a,ar1) c= Ball (a,r1)
by LMBALL1;
A199:
Ball (a,ar1) c= Ball (a,ar11)
by A197, LMBALL1;
A200:
for x being Point of E st x in Ball (a,ar1) holds
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2
proof
let x be
Point of
E;
( x in Ball (a,ar1) implies ||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2 )
assume A201:
x in Ball (
a,
ar1)
;
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2
0. F in Ball (
(0. F),
r1)
by A175, LMBALL2;
then A202:
[x,(0. F)] in [:(Ball (a,r1)),(Ball ((0. F),r1)):]
by A198, A201, ZFMISC_1:87;
reconsider x0F =
[x,(0. F)] as
Point of
[:E,F:] ;
A203:
x in Ball (
a,
ar11)
by A199, A201;
0. F in Ball (
(0. F),
ar12)
by A192, LMBALL2;
then
[x,(0. F)] in [:(Ball (a,ar12)),(Ball ((0. F),ar12)):]
by A195, A203, ZFMISC_1:87;
then
x0F in Ball (
a0F,
ar10)
by A192;
then
ex
q being
Element of
[:E,F:] st
(
q = x0F &
||.(a0F - q).|| < ar10 )
;
then
||.(x0F - a0F).|| < ar10
by NORMSP_1:7;
then A204:
||.((Fai /. x0F) - (Fai /. a0F)).|| < (1 / 2) * r2
by A176, A191, A202;
Fai /. a0F = 0. F
by A146, A167, A168, PARTFUN1:def 6;
hence
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2
by A204, RLVECT_1:13;
verum
end;
reconsider r0 = min ((r1 / 2),ar1) as Real ;
A205:
0 < r1 / 2
by A175, XREAL_1:215;
then A206:
0 < r0
by A196, XXREAL_0:21;
A207:
r0 <= r1 / 2
by XXREAL_0:17;
r1 / 2 < r1
by A175, XREAL_1:216;
then
r0 < r1
by A207, XXREAL_0:2;
then A208:
Ball (a,r0) c= Ball (a,r1)
by LMBALL1;
A209:
for x being Point of E st x in Ball (a,r0) holds
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2
take
r0
; ex r2 being Real st
( 0 < r0 & 0 < r2 & [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
take
r2
; ( 0 < r0 & 0 < r2 & [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
thus
( 0 < r0 & 0 < r2 )
by A196, A205, XXREAL_0:21; ( [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
A211:
cl_Ball ((0. F),r2) c= Ball ((0. F),r1)
by A175, LMBALL1X, XREAL_1:216;
then
[:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= [:(Ball (a,r1)),(Ball ((0. F),r1)):]
by A208, ZFMISC_1:96;
then A212:
[:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= Z1
by A176, XBOOLE_1:1;
A213:
for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball ((0. F),r2) & y2 in cl_Ball ((0. F),r2) holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).||
proof
let x be
Point of
E;
( x in Ball (a,r0) implies for y1, y2 being Point of F st y1 in cl_Ball ((0. F),r2) & y2 in cl_Ball ((0. F),r2) holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).|| )
assume A214:
x in Ball (
a,
r0)
;
for y1, y2 being Point of F st y1 in cl_Ball ((0. F),r2) & y2 in cl_Ball ((0. F),r2) holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).||
let y1,
y2 be
Point of
F;
( y1 in cl_Ball ((0. F),r2) & y2 in cl_Ball ((0. F),r2) implies ||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).|| )
assume that A215:
y1 in cl_Ball (
(0. F),
r2)
and A216:
y2 in cl_Ball (
(0. F),
r2)
;
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).||
A217:
[.y1,y2.] c= cl_Ball (
(0. F),
r2)
by A215, A216, LMCLOSE2;
A218:
].y1,y2.[ c= [.y1,y2.]
by XBOOLE_1:36;
reconsider s =
[x,y1] as
Point of
[:E,F:] ;
reconsider Fs =
Fai * (reproj2 s) as
PartFunc of
F,
F ;
A219:
for
y being
object st
y in [.y1,y2.] holds
y in dom Fs
proof
let y be
object ;
( y in [.y1,y2.] implies y in dom Fs )
assume A220:
y in [.y1,y2.]
;
y in dom Fs
then
[x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A214, A217, ZFMISC_1:87;
then A221:
[x,y] in Z1
by A212;
A222:
y in the
carrier of
F
by A220;
s `1 = x
;
then A223:
(reproj2 s) . y in Z1
by A220, A221, NDIFF_7:def 2;
y in dom (reproj2 s)
by A222, FUNCT_2:def 1;
hence
y in dom Fs
by A146, A223, FUNCT_1:11;
verum
end;
A224:
for
y being
Point of
F st
y in [.y1,y2.] holds
Fs is_differentiable_in y
proof
let y be
Point of
F;
( y in [.y1,y2.] implies Fs is_differentiable_in y )
assume
y in [.y1,y2.]
;
Fs is_differentiable_in y
then A225:
[x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A214, A217, ZFMISC_1:87;
reconsider s1 =
[x,y] as
Point of
[:E,F:] ;
A226:
Fai * (reproj2 s1) is_differentiable_in s1 `2
by A91, A212, A225;
s1 `1 = s `1
;
hence
Fs is_differentiable_in y
by A226, REP2;
verum
end;
A227:
for
y being
Point of
F st
y in [.y1,y2.] holds
Fs is_continuous_in y
by A224, NDIFF_1:44;
A228:
for
y being
Point of
F st
y in ].y1,y2.[ holds
Fs is_differentiable_in y
by A218, A224;
A229:
for
y being
Point of
F st
y in ].y1,y2.[ holds
||.(diff (Fs,y)).|| <= 1
/ 2
proof
let y be
Point of
F;
( y in ].y1,y2.[ implies ||.(diff (Fs,y)).|| <= 1 / 2 )
assume
y in ].y1,y2.[
;
||.(diff (Fs,y)).|| <= 1 / 2
then A230:
y in [.y1,y2.]
by A218;
then A231:
y in cl_Ball (
(0. F),
r2)
by A217;
A232:
[x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A214, A217, A230, ZFMISC_1:87;
reconsider s1 =
[x,y] as
Point of
[:E,F:] ;
||.((Fai `partial`2| Z1) /. [x,y]).|| <= 1
/ 4
by A188, A208, A211, A214, A231;
then A233:
||.(diff ((Fai * (reproj2 s1)),(s1 `2))).|| <= 1
/ 4
by A177, A212, A232;
s1 `1 = s `1
;
then
Fai * (reproj2 s1) = Fs
by REP2;
hence
||.(diff (Fs,y)).|| <= 1
/ 2
by A233, XXREAL_0:2;
verum
end;
A234:
||.((Fs /. y2) - (Fs /. y1)).|| <= (1 / 2) * ||.(y2 - y1).||
by A219, A227, A228, A229, NDIFF_5:19, TARSKI:def 3;
(
[x,y1] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] &
[x,y2] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] )
by A214, A215, A216, ZFMISC_1:87;
then A237:
(
[x,y1] in Z1 &
[x,y2] in Z1 )
by A212;
A235:
dom (reproj2 s) = the
carrier of
F
by FUNCT_2:def 1;
A236:
(
y1 in [.y1,y2.] &
y2 in [.y1,y2.] )
by RLTOPSP1:68;
then A238:
Fs /. y1 =
(Fai * (reproj2 s)) . y1
by A219, PARTFUN1:def 6
.=
Fai . ((reproj2 s) . y1)
by A235, FUNCT_1:13
.=
Fai . [(s `1),y1]
by NDIFF_7:def 2
.=
Fai /. [x,y1]
by A146, A237, PARTFUN1:def 6
;
A239:
Fs /. y2 =
(Fai * (reproj2 s)) . y2
by A219, A236, PARTFUN1:def 6
.=
Fai . ((reproj2 s) . y2)
by A235, FUNCT_1:13
.=
Fai . [(s `1),y2]
by NDIFF_7:def 2
.=
Fai /. [x,y2]
by A146, A237, PARTFUN1:def 6
;
||.((Fs /. y2) - (Fs /. y1)).|| = ||.((Fai /. [x,y1]) - (Fai /. [x,y2])).||
by A238, A239, NORMSP_1:7;
hence
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).||
by A234, NORMSP_1:7;
verum
end;
A240:
for x being Point of E
for y being Point of F st x in Ball (a,r0) & y in cl_Ball ((0. F),r2) holds
Fai . (x,y) in cl_Ball ((0. F),r2)
proof
let x be
Point of
E;
for y being Point of F st x in Ball (a,r0) & y in cl_Ball ((0. F),r2) holds
Fai . (x,y) in cl_Ball ((0. F),r2)let y be
Point of
F;
( x in Ball (a,r0) & y in cl_Ball ((0. F),r2) implies Fai . (x,y) in cl_Ball ((0. F),r2) )
assume A241:
(
x in Ball (
a,
r0) &
y in cl_Ball (
(0. F),
r2) )
;
Fai . (x,y) in cl_Ball ((0. F),r2)
then
[x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by ZFMISC_1:87;
then A242:
[x,y] in Z1
by A212;
A243:
0. F in cl_Ball (
(0. F),
r2)
by A205, LMBALL2;
ex
p being
Point of
F st
(
p = y &
||.((0. F) - p).|| <= r2 )
by A241;
then
||.(y - (0. F)).|| <= r2
by NORMSP_1:7;
then A244:
(1 / 2) * ||.(y - (0. F)).|| <= (1 / 2) * r2
by XREAL_1:64;
A245:
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2
by A209, A241;
||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| <= (1 / 2) * ||.(y - (0. F)).||
by A213, A241, A243;
then A246:
||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| <= (1 / 2) * r2
by A244, XXREAL_0:2;
A247:
Fai . (
x,
y)
= Fai /. [x,y]
by A146, A242, PARTFUN1:def 6;
then reconsider Fxy =
Fai . (
x,
y) as
Point of
F ;
Fxy - (0. F) =
(Fai /. [x,y]) - ((Fai /. [x,(0. F)]) - (Fai /. [x,(0. F)]))
by A247, RLVECT_1:15
.=
((Fai /. [x,y]) - (Fai /. [x,(0. F)])) + (Fai /. [x,(0. F)])
by RLVECT_1:29
;
then A248:
||.(Fxy - (0. F)).|| <= ||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| + ||.(Fai /. [x,(0. F)]).||
by NORMSP_1:def 1;
||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| + ||.(Fai /. [x,(0. F)]).|| <= ((1 / 2) * r2) + ((1 / 2) * r2)
by A245, A246, XREAL_1:7;
then
||.(Fxy - (0. F)).|| <= r2
by A248, XXREAL_0:2;
then
||.((0. F) - Fxy).|| <= r2
by NORMSP_1:7;
hence
Fai . (
x,
y)
in cl_Ball (
(0. F),
r2)
;
verum
end;
A249:
[:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= dom Fai
by A212, FUNCT_2:def 1;
A251:
Ball (a,r0) <> {}
by A206, LMBALL2;
A252:
cl_Ball ((0. F),r2) <> {}
by A205, LMBALL2;
A253:
for y being Point of F st y in cl_Ball ((0. F),r2) holds
for x0 being Point of E st x0 in Ball (a,r0) holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
proof
let y be
Point of
F;
( y in cl_Ball ((0. F),r2) implies for x0 being Point of E st x0 in Ball (a,r0) holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) )
assume A254:
y in cl_Ball (
(0. F),
r2)
;
for x0 being Point of E st x0 in Ball (a,r0) holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
let x0 be
Point of
E;
( x0 in Ball (a,r0) implies for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) )
assume
x0 in Ball (
a,
r0)
;
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
then A257:
[x0,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A254, ZFMISC_1:87;
reconsider z0 =
[x0,y] as
Point of
[:E,F:] ;
let e be
Real;
( 0 < e implies ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) )
assume A256:
0 < e
;
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
consider s being
Real such that A258:
(
0 < s & ( for
z1 being
Point of
[:E,F:] st
z1 in Z1 &
||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < e ) )
by A60, A212, A256, A257;
take
s
;
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
thus
0 < s
by A258;
for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e
let x1 be
Point of
E;
( x1 in Ball (a,r0) & ||.(x1 - x0).|| < s implies ||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e )
assume A259:
(
x1 in Ball (
a,
r0) &
||.(x1 - x0).|| < s )
;
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e
then A260:
[x1,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A254, ZFMISC_1:87;
reconsider z1 =
[x1,y] as
Point of
[:E,F:] ;
- z0 = [(- x0),(- y)]
by PRVECT_3:18;
then z1 - z0 =
[(x1 - x0),(y - y)]
by PRVECT_3:18
.=
[(x1 - x0),(0. F)]
by RLVECT_1:15
;
then
||.(z1 - z0).|| = ||.(x1 - x0).||
by LMNR1;
hence
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e
by A212, A258, A259, A260;
verum
end;
then consider Psi being PartFunc of E,F such that
A262:
( Psi is_continuous_on Ball (a,r0) & dom Psi = Ball (a,r0) & rng Psi c= cl_Ball ((0. F),r2) & ( for x being Point of E st x in Ball (a,r0) holds
Fai . (x,(Psi . x)) = Psi . x ) )
by A213, A240, A249, A251, A252, FIXPOINT3;
for z being object holds
( z in cl_Ball (b,r2) iff z in { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) } )
then A267:
cl_Ball (b,r2) = { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) }
by TARSKI:2;
A268:
K .: [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= K .: Z1
by A212, RELAT_1:123;
A269: K .: Z1 =
H " (H .: Z)
by A19, A20, FUNCT_1:85
.=
Z
by A15, A19, FUNCT_1:94
;
for y being object holds
( y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] iff ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) )
proof
let y be
object ;
( y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] iff ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) )
hereby ( ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) implies y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] )
assume
y in [:(Ball (a,r0)),(cl_Ball (b,r2)):]
;
ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x )then consider d,
w being
object such that A270:
(
d in Ball (
a,
r0) &
w in cl_Ball (
b,
r2) &
y = [d,w] )
by ZFMISC_1:def 2;
reconsider d =
d as
Point of
E by A270;
reconsider w =
w as
Point of
F by A270;
reconsider b2 =
w - b as
Point of
F ;
reconsider p =
[d,b2] as
Point of
[:E,F:] ;
consider y0 being
Point of
F such that A271:
(
w = y0 + b &
y0 in cl_Ball (
(0. F),
r2) )
by A267, A270;
A272:
w - b =
y0 + (b - b)
by A271, RLVECT_1:28
.=
y0 + (0. F)
by RLVECT_1:15
.=
y0
by RLVECT_1:def 4
;
then y =
[(d + (0. E)),(b2 + b)]
by A270, A271, RLVECT_1:def 4
.=
p + e0b
by PRVECT_3:18
.=
(1 * p) + e0b
by RLVECT_1:def 8
.=
K . p
by A16
;
hence
ex
x being
object st
(
x in dom K &
x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] &
y = K . x )
by A17, A270, A271, A272, ZFMISC_1:87;
verum
end;
given x being
object such that A273:
(
x in dom K &
x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] &
y = K . x )
;
y in [:(Ball (a,r0)),(cl_Ball (b,r2)):]
reconsider p =
x as
Point of
[:E,F:] by A273;
A274:
K . x =
(1 * p) + e0b
by A16
.=
p + e0b
by RLVECT_1:def 8
;
consider z being
Point of
E,
w being
Point of
F such that A275:
p = [z,w]
by PRVECT_3:18;
A276:
p + e0b =
[(z + (0. E)),(w + b)]
by A275, PRVECT_3:18
.=
[z,(w + b)]
by RLVECT_1:def 4
;
A277:
(
z in Ball (
a,
r0) &
w in cl_Ball (
(0. F),
r2) )
by A273, A275, ZFMISC_1:87;
then
w + b in cl_Ball (
b,
r2)
by A267;
hence
y in [:(Ball (a,r0)),(cl_Ball (b,r2)):]
by A273, A274, A276, A277, ZFMISC_1:87;
verum
end;
hence
[:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z
by A268, A269, FUNCT_1:def 6; ( ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
deffunc H3( object ) -> Element of the carrier of F = (Psi /. $1) + b;
A278:
for y being object st y in Ball (a,r0) holds
H3(y) in cl_Ball (b,r2)
proof
let y be
object ;
( y in Ball (a,r0) implies H3(y) in cl_Ball (b,r2) )
assume A279:
y in Ball (
a,
r0)
;
H3(y) in cl_Ball (b,r2)
reconsider yp =
y as
Point of
E by A279;
Psi . yp in rng Psi
by A262, A279, FUNCT_1:3;
then
Psi . yp in cl_Ball (
(0. F),
r2)
by A262;
then
Psi /. yp in cl_Ball (
(0. F),
r2)
by A262, A279, PARTFUN1:def 6;
hence
H3(
y)
in cl_Ball (
b,
r2)
by A267;
verum
end;
consider Eta being Function of (Ball (a,r0)),(cl_Ball (b,r2)) such that
A280:
for y being object st y in Ball (a,r0) holds
Eta . y = H3(y)
from FUNCT_2:sch 2(A278);
A281:
rng Eta c= cl_Ball (b,r2)
;
cl_Ball (b,r2) <> {}
by A205, LMBALL2;
then A282:
dom Eta = Ball (a,r0)
by FUNCT_2:def 1;
rng Eta c= the carrier of F
by XBOOLE_1:1;
then reconsider Eta = Eta as PartFunc of E,F by A282, RELSET_1:4;
A284:
for x0 being Point of E
for r being Real st x0 in Ball (a,r0) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) )
proof
let x0 be
Point of
E;
for r being Real st x0 in Ball (a,r0) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) )let r be
Real;
( x0 in Ball (a,r0) & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) ) )
assume A285:
(
x0 in Ball (
a,
r0) &
0 < r )
;
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) )
then consider s being
Real such that A286:
(
0 < s & ( for
x1 being
Point of
E st
x1 in Ball (
a,
r0) &
||.(x1 - x0).|| < s holds
||.((Psi /. x1) - (Psi /. x0)).|| < r ) )
by A262, NFCONT_1:19;
take
s
;
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) )
thus
0 < s
by A286;
for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r
let x1 be
Point of
E;
( x1 in Ball (a,r0) & ||.(x1 - x0).|| < s implies ||.((Eta /. x1) - (Eta /. x0)).|| < r )
assume A287:
(
x1 in Ball (
a,
r0) &
||.(x1 - x0).|| < s )
;
||.((Eta /. x1) - (Eta /. x0)).|| < r
then A288:
Eta /. x1 =
Eta . x1
by A282, PARTFUN1:def 6
.=
(Psi /. x1) + b
by A280, A287
;
Eta /. x0 =
Eta . x0
by A282, A285, PARTFUN1:def 6
.=
(Psi /. x0) + b
by A280, A285
;
then (Eta /. x1) - (Eta /. x0) =
(((Psi /. x1) + b) - b) - (Psi /. x0)
by A288, RLVECT_1:27
.=
(Psi /. x1) - (Psi /. x0)
by RLVECT_4:1
;
hence
||.((Eta /. x1) - (Eta /. x0)).|| < r
by A286, A287;
verum
end;
A290:
for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta . x)) = c
proof
let x be
Point of
E;
( x in Ball (a,r0) implies f . (x,(Eta . x)) = c )
assume A291:
x in Ball (
a,
r0)
;
f . (x,(Eta . x)) = c
then A292:
Psi . x in rng Psi
by A262, FUNCT_1:3;
then reconsider y =
Psi . x as
Point of
F ;
A293:
(
y in cl_Ball (
(0. F),
r2) &
Fai . (
x,
y)
= y )
by A262, A291, A292;
A294:
[x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A262, A291, A292, ZFMISC_1:87;
then
y = y - (f2 /. [x,y])
by A58, A212, A293;
then
- (- (f2 /. [x,y])) = - (0. F)
by RLVECT_1:9;
then
f2 /. [x,y] = - (0. F)
by RLVECT_1:17;
then A295:
f2 /. [x,y] = 0. F
by RLVECT_1:12;
f2 . (
x,
y)
= f2 /. [x,y]
by A50, A212, A294, PARTFUN1:def 6;
then A296:
Q . (f1 . (x,y)) = 0. F
by A51, A212, A294, A295;
f1 . (
x,
y)
= f1 /. [x,y]
by A41, A212, A294, PARTFUN1:def 6;
then
f1 . (
x,
y)
= 0. G
by A8, A10, A296, LQ2;
then
0. G = (f /. [x,(y + b)]) - c
by A42, A212, A294;
then A297:
f /. [x,(y + b)] = c
by RLVECT_1:21;
y + b =
(Psi /. x) + b
by A262, A291, PARTFUN1:def 6
.=
Eta . x
by A280, A291
;
hence
f . (
x,
(Eta . x))
= c
by A2, A21, A212, A294, A297, PARTFUN1:def 6;
verum
end;
A298:
for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c )
proof
let x be
Point of
E;
( x in Ball (a,r0) implies ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) )
assume A299:
x in Ball (
a,
r0)
;
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c )
then A300:
Eta . x in rng Eta
by A282, FUNCT_1:3;
then reconsider y =
Eta . x as
Point of
F ;
take
y
;
( y in cl_Ball (b,r2) & f . (x,y) = c )
thus
y in cl_Ball (
b,
r2)
by A281, A300;
f . (x,y) = c
thus
f . (
x,
y)
= c
by A290, A299;
verum
end;
A301:
for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2
proof
let x be
Point of
E;
( x in Ball (a,r0) implies for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 )
assume A302:
x in Ball (
a,
r0)
;
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2
let y1,
y2 be
Point of
F;
( y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c implies y1 = y2 )
assume A303:
(
y1 in cl_Ball (
b,
r2) &
y2 in cl_Ball (
b,
r2) &
f . (
x,
y1)
= c &
f . (
x,
y2)
= c )
;
y1 = y2
then consider y10 being
Point of
F such that A304:
(
y1 = y10 + b &
y10 in cl_Ball (
(0. F),
r2) )
by A267;
consider y20 being
Point of
F such that A305:
(
y2 = y20 + b &
y20 in cl_Ball (
(0. F),
r2) )
by A267, A303;
A306:
[x,y10] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A302, A304, ZFMISC_1:87;
A307:
[x,y20] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A302, A305, ZFMISC_1:87;
A308:
[x,y10] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A302, A304, ZFMISC_1:87;
A309:
[x,y20] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):]
by A302, A305, ZFMISC_1:87;
f . (
x,
y1)
= f /. [x,y1]
by A2, A21, A212, A304, A306, PARTFUN1:def 6;
then
(f /. [x,(y10 + b)]) - c = 0. G
by A303, A304, RLVECT_1:5;
then
f1 . (
x,
y10)
= 0. G
by A42, A212, A308;
then
Q . (f1 . (x,y10)) = 0. F
by LOPBAN_7:3;
then
f2 . (
x,
y10)
= 0. F
by A51, A212, A308;
then
f2 /. [x,y10] = 0. F
by A50, A212, A308, PARTFUN1:def 6;
then A311:
Fai . (
x,
y10) =
y10 - (0. F)
by A58, A212, A308
.=
y10
by RLVECT_1:13
;
f . (
x,
y2)
= f /. [x,y2]
by A2, A21, A212, A305, A307, PARTFUN1:def 6;
then
(f /. [x,(y20 + b)]) - c = 0. G
by A303, A305, RLVECT_1:5;
then
f1 . (
x,
y20)
= 0. G
by A42, A212, A309;
then
Q . (f1 . (x,y20)) = 0. F
by LOPBAN_7:3;
then
f2 . (
x,
y20)
= 0. F
by A51, A212, A309;
then
f2 /. [x,y20] = 0. F
by A50, A212, A309, PARTFUN1:def 6;
then Fai . (
x,
y20) =
y20 - (0. F)
by A58, A212, A309
.=
y20
by RLVECT_1:13
;
hence
y1 = y2
by A213, A240, A249, A253, A302, A304, A305, A311, FIXPOINT2;
verum
end;
A313:
( a in Ball (a,r0) & b in cl_Ball (b,r2) )
by A206, A207, LMBALL2;
A314:
Eta . a in rng Eta
by A206, A282, FUNCT_1:3, LMBALL2;
f . (a,(Eta . a)) = c
by A206, A290, LMBALL2;
then A315:
Eta . a = b
by A7, A281, A301, A313, A314;
for Eta1, Eta2 being PartFunc of E,F st dom Eta1 = Ball (a,r0) & rng Eta1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta1 . x)) = c ) & dom Eta2 = Ball (a,r0) & rng Eta2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta2 . x)) = c ) holds
Eta1 = Eta2
proof
let Eta1,
Eta2 be
PartFunc of
E,
F;
( dom Eta1 = Ball (a,r0) & rng Eta1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta1 . x)) = c ) & dom Eta2 = Ball (a,r0) & rng Eta2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta2 . x)) = c ) implies Eta1 = Eta2 )
assume that A316:
(
dom Eta1 = Ball (
a,
r0) &
rng Eta1 c= cl_Ball (
b,
r2) & ( for
x being
Point of
E st
x in Ball (
a,
r0) holds
f . (
x,
(Eta1 . x))
= c ) )
and A317:
(
dom Eta2 = Ball (
a,
r0) &
rng Eta2 c= cl_Ball (
b,
r2) & ( for
x being
Point of
E st
x in Ball (
a,
r0) holds
f . (
x,
(Eta2 . x))
= c ) )
;
Eta1 = Eta2
for
x being
object st
x in dom Eta1 holds
Eta1 . x = Eta2 . x
proof
let x0 be
object ;
( x0 in dom Eta1 implies Eta1 . x0 = Eta2 . x0 )
assume A318:
x0 in dom Eta1
;
Eta1 . x0 = Eta2 . x0
then reconsider x =
x0 as
Point of
E ;
A319:
Eta1 . x0 in rng Eta1
by A318, FUNCT_1:3;
A320:
Eta2 . x0 in rng Eta2
by A316, A317, A318, FUNCT_1:3;
(
f . (
x,
(Eta1 . x))
= c &
f . (
x,
(Eta2 . x))
= c )
by A316, A317, A318;
hence
Eta1 . x0 = Eta2 . x0
by A301, A316, A317, A318, A319, A320;
verum
end;
hence
Eta1 = Eta2
by A316, A317, FUNCT_1:2;
verum
end;
hence
( ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )
by A281, A282, A284, A290, A298, A301, A315, NFCONT_1:19; verum