let E, F be non trivial RealBanachSpace; :: thesis: for D being Subset of E

for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let D be Subset of E; :: thesis: for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let f be PartFunc of E,F; :: thesis: for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let f1 be PartFunc of [:E,F:],F; :: thesis: for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let Z be Subset of [:E,F:]; :: thesis: ( D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) implies ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) ) )

assume that

A1: D is open and

A2: ( dom f = D & D <> {} ) and

A3: f is_differentiable_on D and

A4: f `| D is_continuous_on D and

A5: Z = [:D, the carrier of F:] and

A6: dom f1 = Z and

A7: for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ; :: thesis: ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

A9: Z is open by A1, A5, Th4;

A10: for z being Point of [:E,F:] st z in Z holds

( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) )

then A38: Z = dom (f1 `partial`1| Z) by NDIFF_7:def 10;

for x0 being Point of [:E,F:]

for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

reconsider J = FuncUnit F as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) ;

A51: for z being Point of [:E,F:] st z in Z holds

( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J )

then A85: Z = dom (f1 `partial`2| Z) by NDIFF_7:def 11;

for x0 being Point of [:E,F:]

for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

hence ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z ) by A9, A37, A50, A84, NDIFF_7:52; :: thesis: for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

thus for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) :: thesis: verum

for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let D be Subset of E; :: thesis: for f being PartFunc of E,F

for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let f be PartFunc of E,F; :: thesis: for f1 being PartFunc of [:E,F:],F

for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let f1 be PartFunc of [:E,F:],F; :: thesis: for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) holds

( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

let Z be Subset of [:E,F:]; :: thesis: ( D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ) implies ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) ) )

assume that

A1: D is open and

A2: ( dom f = D & D <> {} ) and

A3: f is_differentiable_on D and

A4: f `| D is_continuous_on D and

A5: Z = [:D, the carrier of F:] and

A6: dom f1 = Z and

A7: for s being Point of E

for t being Point of F st s in D holds

f1 . (s,t) = (f /. s) - t ; :: thesis: ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )

A9: Z is open by A1, A5, Th4;

A10: for z being Point of [:E,F:] st z in Z holds

( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) )

proof

then A37:
f1 is_partial_differentiable_on`1 Z
by A6;
let z be Point of [:E,F:]; :: thesis: ( z in Z implies ( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) ) )

assume A11: z in Z ; :: thesis: ( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) )

consider x being Point of E, y being Point of F such that

A12: z = [x,y] by PRVECT_3:18;

set CST = D --> y;

A13: ( rng (D --> y) = {y} & dom (D --> y) = D ) by A2, FUNCOP_1:8, FUNCOP_1:13;

then reconsider CST = D --> y as PartFunc of E,F by RELSET_1:4;

A14: ( CST is_differentiable_on D & ( for s being Point of E st s in D holds

(CST `| D) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) ) ) by A1, A13, NDIFF_1:33;

A16: dom (f - CST) = D /\ D by A2, A13, VFUNCT_1:def 2

.= D ;

A17: for s being object holds

( s in dom (f1 * (reproj1 z)) iff s in dom (f - CST) )

(f1 * (reproj1 z)) . s = (f - CST) . s

then A33: f is_differentiable_in x by A1, A3, NDIFF_1:31;

CST is_differentiable_in x by A1, A14, A32, NDIFF_1:31;

then A34: ( f - CST is_differentiable_in x & diff ((f - CST),x) = (diff (f,x)) - (diff (CST,x)) ) by A33, NDIFF_1:36;

hence f1 is_partial_differentiable_in`1 z by A12, A17, A24, FUNCT_1:2, TARSKI:2; :: thesis: partdiff`1 (f1,z) = diff (f,(z `1))

A36: diff (CST,x) = (CST `| D) /. x by A14, A32, NDIFF_1:def 9

.= 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) by A1, A13, A32, NDIFF_1:33 ;

thus partdiff`1 (f1,z) = diff ((f - CST),x) by A12, A17, A24, FUNCT_1:2, TARSKI:2

.= diff (f,(z `1)) by A12, A34, A36, RLVECT_1:13 ; :: thesis: verum

end;assume A11: z in Z ; :: thesis: ( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) )

consider x being Point of E, y being Point of F such that

A12: z = [x,y] by PRVECT_3:18;

set CST = D --> y;

A13: ( rng (D --> y) = {y} & dom (D --> y) = D ) by A2, FUNCOP_1:8, FUNCOP_1:13;

then reconsider CST = D --> y as PartFunc of E,F by RELSET_1:4;

A14: ( CST is_differentiable_on D & ( for s being Point of E st s in D holds

(CST `| D) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) ) ) by A1, A13, NDIFF_1:33;

A16: dom (f - CST) = D /\ D by A2, A13, VFUNCT_1:def 2

.= D ;

A17: for s being object holds

( s in dom (f1 * (reproj1 z)) iff s in dom (f - CST) )

proof

A24:
for s being object st s in dom (f1 * (reproj1 z)) holds
let s be object ; :: thesis: ( s in dom (f1 * (reproj1 z)) iff s in dom (f - CST) )

then reconsider t = s as Point of E ;

(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then A23: (reproj1 z) . t in dom f1 by A5, A6, A16, A20, ZFMISC_1:87;

dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;

hence s in dom (f1 * (reproj1 z)) by A23, FUNCT_1:11; :: thesis: verum

end;hereby :: thesis: ( s in dom (f - CST) implies s in dom (f1 * (reproj1 z)) )

assume A20:
s in dom (f - CST)
; :: thesis: s in dom (f1 * (reproj1 z))assume A19:
s in dom (f1 * (reproj1 z))
; :: thesis: s in dom (f - CST)

then reconsider t = s as Point of E ;

(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then [t,y] in dom f1 by A19, FUNCT_1:11;

hence s in dom (f - CST) by A5, A6, A16, ZFMISC_1:87; :: thesis: verum

end;then reconsider t = s as Point of E ;

(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then [t,y] in dom f1 by A19, FUNCT_1:11;

hence s in dom (f - CST) by A5, A6, A16, ZFMISC_1:87; :: thesis: verum

then reconsider t = s as Point of E ;

(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then A23: (reproj1 z) . t in dom f1 by A5, A6, A16, A20, ZFMISC_1:87;

dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;

hence s in dom (f1 * (reproj1 z)) by A23, FUNCT_1:11; :: thesis: verum

(f1 * (reproj1 z)) . s = (f - CST) . s

proof

A32:
x in D
by A5, A11, A12, ZFMISC_1:87;
let s be object ; :: thesis: ( s in dom (f1 * (reproj1 z)) implies (f1 * (reproj1 z)) . s = (f - CST) . s )

assume A25: s in dom (f1 * (reproj1 z)) ; :: thesis: (f1 * (reproj1 z)) . s = (f - CST) . s

then A26: ( s in dom (reproj1 z) & (reproj1 z) . s in dom f1 ) by FUNCT_1:11;

reconsider t = s as Point of E by A25;

A27: (reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then A28: t in D by A5, A6, A26, ZFMISC_1:87;

then A29: CST /. s = CST . s by A13, PARTFUN1:def 6

.= y by A28, FUNCOP_1:7 ;

thus (f1 * (reproj1 z)) . s = f1 . (t,y) by A25, A27, FUNCT_1:12

.= (f /. t) - (CST /. s) by A7, A28, A29

.= (f - CST) /. s by A17, A25, VFUNCT_1:def 2

.= (f - CST) . s by A17, A25, PARTFUN1:def 6 ; :: thesis: verum

end;assume A25: s in dom (f1 * (reproj1 z)) ; :: thesis: (f1 * (reproj1 z)) . s = (f - CST) . s

then A26: ( s in dom (reproj1 z) & (reproj1 z) . s in dom f1 ) by FUNCT_1:11;

reconsider t = s as Point of E by A25;

A27: (reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1

.= [t,y] by A12 ;

then A28: t in D by A5, A6, A26, ZFMISC_1:87;

then A29: CST /. s = CST . s by A13, PARTFUN1:def 6

.= y by A28, FUNCOP_1:7 ;

thus (f1 * (reproj1 z)) . s = f1 . (t,y) by A25, A27, FUNCT_1:12

.= (f /. t) - (CST /. s) by A7, A28, A29

.= (f - CST) /. s by A17, A25, VFUNCT_1:def 2

.= (f - CST) . s by A17, A25, PARTFUN1:def 6 ; :: thesis: verum

then A33: f is_differentiable_in x by A1, A3, NDIFF_1:31;

CST is_differentiable_in x by A1, A14, A32, NDIFF_1:31;

then A34: ( f - CST is_differentiable_in x & diff ((f - CST),x) = (diff (f,x)) - (diff (CST,x)) ) by A33, NDIFF_1:36;

hence f1 is_partial_differentiable_in`1 z by A12, A17, A24, FUNCT_1:2, TARSKI:2; :: thesis: partdiff`1 (f1,z) = diff (f,(z `1))

A36: diff (CST,x) = (CST `| D) /. x by A14, A32, NDIFF_1:def 9

.= 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) by A1, A13, A32, NDIFF_1:33 ;

thus partdiff`1 (f1,z) = diff ((f - CST),x) by A12, A17, A24, FUNCT_1:2, TARSKI:2

.= diff (f,(z `1)) by A12, A34, A36, RLVECT_1:13 ; :: thesis: verum

then A38: Z = dom (f1 `partial`1| Z) by NDIFF_7:def 10;

for x0 being Point of [:E,F:]

for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

proof

then A50:
f1 `partial`1| Z is_continuous_on Z
by A38, NFCONT_1:19;
let x0 be Point of [:E,F:]; :: thesis: for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) ) )

assume A39: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

consider s0 being Point of E, t0 being Point of F such that

A40: x0 = [s0,t0] by PRVECT_3:18;

A41: s0 in D by A5, A39, A40, ZFMISC_1:87;

then consider s being Real such that

A43: ( 0 < s & ( for s1 being Point of E st s1 in D & ||.(s1 - s0).|| < s holds

||.(((f `| D) /. s1) - ((f `| D) /. s0)).|| < r ) ) by A4, A39, NFCONT_1:19;

take s ; :: thesis: ( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

thus 0 < s by A43; :: thesis: for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r

let x1 be Point of [:E,F:]; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r )

assume A44: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r

consider s1 being Point of E, t1 being Point of F such that

A45: x1 = [s1,t1] by PRVECT_3:18;

A46: s1 in D by A5, A44, A45, ZFMISC_1:87;

- x0 = [(- s0),(- t0)] by A40, PRVECT_3:18;

then x1 - x0 = [(s1 - s0),(t1 - t0)] by A45, PRVECT_3:18;

then ||.(s1 - s0).|| <= ||.(x1 - x0).|| by LOPBAN_7:15;

then A48: ||.(s1 - s0).|| < s by A44, XXREAL_0:2;

A49: (f `| D) /. s1 = diff (f,(x1 `1)) by A3, A45, A46, NDIFF_1:def 9

.= partdiff`1 (f1,x1) by A10, A44

.= (f1 `partial`1| Z) /. x1 by A37, A44, NDIFF_7:def 10 ;

(f `| D) /. s0 = diff (f,(x0 `1)) by A3, A40, A41, NDIFF_1:def 9

.= partdiff`1 (f1,x0) by A10, A39

.= (f1 `partial`1| Z) /. x0 by A37, A39, NDIFF_7:def 10 ;

hence ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r by A43, A46, A48, A49; :: thesis: verum

end;ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) ) )

assume A39: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

consider s0 being Point of E, t0 being Point of F such that

A40: x0 = [s0,t0] by PRVECT_3:18;

A41: s0 in D by A5, A39, A40, ZFMISC_1:87;

then consider s being Real such that

A43: ( 0 < s & ( for s1 being Point of E st s1 in D & ||.(s1 - s0).|| < s holds

||.(((f `| D) /. s1) - ((f `| D) /. s0)).|| < r ) ) by A4, A39, NFCONT_1:19;

take s ; :: thesis: ( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

thus 0 < s by A43; :: thesis: for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r

let x1 be Point of [:E,F:]; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r )

assume A44: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r

consider s1 being Point of E, t1 being Point of F such that

A45: x1 = [s1,t1] by PRVECT_3:18;

A46: s1 in D by A5, A44, A45, ZFMISC_1:87;

- x0 = [(- s0),(- t0)] by A40, PRVECT_3:18;

then x1 - x0 = [(s1 - s0),(t1 - t0)] by A45, PRVECT_3:18;

then ||.(s1 - s0).|| <= ||.(x1 - x0).|| by LOPBAN_7:15;

then A48: ||.(s1 - s0).|| < s by A44, XXREAL_0:2;

A49: (f `| D) /. s1 = diff (f,(x1 `1)) by A3, A45, A46, NDIFF_1:def 9

.= partdiff`1 (f1,x1) by A10, A44

.= (f1 `partial`1| Z) /. x1 by A37, A44, NDIFF_7:def 10 ;

(f `| D) /. s0 = diff (f,(x0 `1)) by A3, A40, A41, NDIFF_1:def 9

.= partdiff`1 (f1,x0) by A10, A39

.= (f1 `partial`1| Z) /. x0 by A37, A39, NDIFF_7:def 10 ;

hence ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r by A43, A46, A48, A49; :: thesis: verum

reconsider J = FuncUnit F as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) ;

A51: for z being Point of [:E,F:] st z in Z holds

( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J )

proof

then A84:
f1 is_partial_differentiable_on`2 Z
by A6;
let z be Point of [:E,F:]; :: thesis: ( z in Z implies ( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J ) )

assume A52: z in Z ; :: thesis: ( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J )

the carrier of F c= the carrier of F ;

then reconsider CF = the carrier of F as Subset of F ;

for y being Point of F st y in CF holds

ex r being Real st

( 0 < r & Ball (y,r) c= CF )

consider x being Point of E, y being Point of F such that

A54: z = [x,y] by PRVECT_3:18;

A55: x in D by A5, A52, A54, ZFMISC_1:87;

set fx = CF --> (f /. x);

A57: ( rng (CF --> (f /. x)) = {(f /. x)} & dom (CF --> (f /. x)) = CF ) by FUNCOP_1:8, FUNCOP_1:13;

reconsider fx = CF --> (f /. x) as PartFunc of F,F ;

A58: ( fx is_differentiable_on CF & ( for s being Point of F st s in CF holds

(fx `| CF) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ) ) by A53, A57, NDIFF_1:33;

set I = id CF;

A59: ( dom (id CF) = CF & rng (id CF) = CF ) ;

A60: (id CF) | CF = id CF ;

reconsider I = id CF as PartFunc of F,F ;

A61: ( I is_differentiable_on CF & ( for s being Point of F st s in CF holds

(I `| CF) /. s = id CF ) ) by A53, A59, A60, NDIFF_1:38;

( dom (fx - I) = (dom fx) /\ (dom I) & ( for s being Element of F st s in dom (fx - I) holds

(fx - I) /. s = (fx /. s) - (I /. s) ) ) by VFUNCT_1:def 2;

then A63: dom (fx - I) = CF /\ CF by FUNCOP_1:13

.= CF ;

A64: for s being object holds

( s in dom (f1 * (reproj2 z)) iff s in dom (fx - I) )

(f1 * (reproj2 z)) . s = (fx - I) . s

I is_differentiable_in y by A53, A61, NDIFF_1:31;

then A80: ( fx - I is_differentiable_in y & diff ((fx - I),y) = (diff (fx,y)) - (diff (I,y)) ) by A79, NDIFF_1:36;

hence f1 is_partial_differentiable_in`2 z by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis: partdiff`2 (f1,z) = - J

A82: diff (I,y) = (I `| CF) /. y by A61, NDIFF_1:def 9

.= J by A53, A59, A60, NDIFF_1:38 ;

diff (fx,y) = (fx `| CF) /. y by A58, NDIFF_1:def 9

.= 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A53, A57, NDIFF_1:33 ;

then diff ((fx - I),y) = - J by A80, A82, RLVECT_1:14;

hence partdiff`2 (f1,z) = - J by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis: verum

end;assume A52: z in Z ; :: thesis: ( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J )

the carrier of F c= the carrier of F ;

then reconsider CF = the carrier of F as Subset of F ;

for y being Point of F st y in CF holds

ex r being Real st

( 0 < r & Ball (y,r) c= CF )

proof

then A53:
CF is open
by NDIFF_8:20;
let y be Point of F; :: thesis: ( y in CF implies ex r being Real st

( 0 < r & Ball (y,r) c= CF ) )

assume y in CF ; :: thesis: ex r being Real st

( 0 < r & Ball (y,r) c= CF )

take r = 1; :: thesis: ( 0 < r & Ball (y,r) c= CF )

thus 0 < r ; :: thesis: Ball (y,r) c= CF

thus Ball (y,r) c= CF ; :: thesis: verum

end;( 0 < r & Ball (y,r) c= CF ) )

assume y in CF ; :: thesis: ex r being Real st

( 0 < r & Ball (y,r) c= CF )

take r = 1; :: thesis: ( 0 < r & Ball (y,r) c= CF )

thus 0 < r ; :: thesis: Ball (y,r) c= CF

thus Ball (y,r) c= CF ; :: thesis: verum

consider x being Point of E, y being Point of F such that

A54: z = [x,y] by PRVECT_3:18;

A55: x in D by A5, A52, A54, ZFMISC_1:87;

set fx = CF --> (f /. x);

A57: ( rng (CF --> (f /. x)) = {(f /. x)} & dom (CF --> (f /. x)) = CF ) by FUNCOP_1:8, FUNCOP_1:13;

reconsider fx = CF --> (f /. x) as PartFunc of F,F ;

A58: ( fx is_differentiable_on CF & ( for s being Point of F st s in CF holds

(fx `| CF) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ) ) by A53, A57, NDIFF_1:33;

set I = id CF;

A59: ( dom (id CF) = CF & rng (id CF) = CF ) ;

A60: (id CF) | CF = id CF ;

reconsider I = id CF as PartFunc of F,F ;

A61: ( I is_differentiable_on CF & ( for s being Point of F st s in CF holds

(I `| CF) /. s = id CF ) ) by A53, A59, A60, NDIFF_1:38;

( dom (fx - I) = (dom fx) /\ (dom I) & ( for s being Element of F st s in dom (fx - I) holds

(fx - I) /. s = (fx /. s) - (I /. s) ) ) by VFUNCT_1:def 2;

then A63: dom (fx - I) = CF /\ CF by FUNCOP_1:13

.= CF ;

A64: for s being object holds

( s in dom (f1 * (reproj2 z)) iff s in dom (fx - I) )

proof

A71:
for s being object st s in dom (f1 * (reproj2 z)) holds
let s be object ; :: thesis: ( s in dom (f1 * (reproj2 z)) iff s in dom (fx - I) )

A66: ( s in dom (f1 * (reproj2 z)) iff ( s in dom (reproj2 z) & (reproj2 z) . s in dom f1 ) ) by FUNCT_1:11;

thus ( s in dom (f1 * (reproj2 z)) implies s in dom (fx - I) ) by A63; :: thesis: ( s in dom (fx - I) implies s in dom (f1 * (reproj2 z)) )

assume s in dom (fx - I) ; :: thesis: s in dom (f1 * (reproj2 z))

then reconsider t = s as Point of F ;

A69: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2

.= [x,t] by A54 ;

dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;

hence s in dom (f1 * (reproj2 z)) by A5, A6, A55, A66, A69, ZFMISC_1:87; :: thesis: verum

end;A66: ( s in dom (f1 * (reproj2 z)) iff ( s in dom (reproj2 z) & (reproj2 z) . s in dom f1 ) ) by FUNCT_1:11;

thus ( s in dom (f1 * (reproj2 z)) implies s in dom (fx - I) ) by A63; :: thesis: ( s in dom (fx - I) implies s in dom (f1 * (reproj2 z)) )

assume s in dom (fx - I) ; :: thesis: s in dom (f1 * (reproj2 z))

then reconsider t = s as Point of F ;

A69: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2

.= [x,t] by A54 ;

dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;

hence s in dom (f1 * (reproj2 z)) by A5, A6, A55, A66, A69, ZFMISC_1:87; :: thesis: verum

(f1 * (reproj2 z)) . s = (fx - I) . s

proof

A79:
fx is_differentiable_in y
by A53, A58, NDIFF_1:31;
let s be object ; :: thesis: ( s in dom (f1 * (reproj2 z)) implies (f1 * (reproj2 z)) . s = (fx - I) . s )

assume A72: s in dom (f1 * (reproj2 z)) ; :: thesis: (f1 * (reproj2 z)) . s = (fx - I) . s

then reconsider t = s as Point of F ;

A73: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2

.= [x,t] by A54 ;

A74: t in CF ;

then A75: I /. s = I . s by A59, PARTFUN1:def 6

.= s by A74 ;

A76: fx /. s = fx . s by A57, A74, PARTFUN1:def 6

.= f /. x by A74, FUNCOP_1:7 ;

thus (f1 * (reproj2 z)) . s = f1 . (x,t) by A72, A73, FUNCT_1:12

.= (f /. x) - (I /. s) by A7, A55, A75

.= (fx - I) /. s by A64, A72, A76, VFUNCT_1:def 2

.= (fx - I) . s by A64, A72, PARTFUN1:def 6 ; :: thesis: verum

end;assume A72: s in dom (f1 * (reproj2 z)) ; :: thesis: (f1 * (reproj2 z)) . s = (fx - I) . s

then reconsider t = s as Point of F ;

A73: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2

.= [x,t] by A54 ;

A74: t in CF ;

then A75: I /. s = I . s by A59, PARTFUN1:def 6

.= s by A74 ;

A76: fx /. s = fx . s by A57, A74, PARTFUN1:def 6

.= f /. x by A74, FUNCOP_1:7 ;

thus (f1 * (reproj2 z)) . s = f1 . (x,t) by A72, A73, FUNCT_1:12

.= (f /. x) - (I /. s) by A7, A55, A75

.= (fx - I) /. s by A64, A72, A76, VFUNCT_1:def 2

.= (fx - I) . s by A64, A72, PARTFUN1:def 6 ; :: thesis: verum

I is_differentiable_in y by A53, A61, NDIFF_1:31;

then A80: ( fx - I is_differentiable_in y & diff ((fx - I),y) = (diff (fx,y)) - (diff (I,y)) ) by A79, NDIFF_1:36;

hence f1 is_partial_differentiable_in`2 z by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis: partdiff`2 (f1,z) = - J

A82: diff (I,y) = (I `| CF) /. y by A61, NDIFF_1:def 9

.= J by A53, A59, A60, NDIFF_1:38 ;

diff (fx,y) = (fx `| CF) /. y by A58, NDIFF_1:def 9

.= 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A53, A57, NDIFF_1:33 ;

then diff ((fx - I),y) = - J by A80, A82, RLVECT_1:14;

hence partdiff`2 (f1,z) = - J by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis: verum

then A85: Z = dom (f1 `partial`2| Z) by NDIFF_7:def 11;

for x0 being Point of [:E,F:]

for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

proof

then
f1 `partial`2| Z is_continuous_on Z
by A85, NFCONT_1:19;
let x0 be Point of [:E,F:]; :: thesis: for r being Real st x0 in Z & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) ) )

assume A86: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

take s = 1; :: thesis: ( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

thus 0 < s ; :: thesis: for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r

let x1 be Point of [:E,F:]; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r )

assume A88: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r

A90: - J = partdiff`2 (f1,x1) by A51, A88

.= (f1 `partial`2| Z) /. x1 by A84, A88, NDIFF_7:def 11 ;

- J = partdiff`2 (f1,x0) by A51, A86

.= (f1 `partial`2| Z) /. x0 by A84, A86, NDIFF_7:def 11 ;

then ((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0) = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A90, RLVECT_1:15;

hence ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r by A86, NORMSP_0:def 6; :: thesis: verum

end;ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) ) )

assume A86: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

take s = 1; :: thesis: ( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

thus 0 < s ; :: thesis: for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds

||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r

let x1 be Point of [:E,F:]; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r )

assume A88: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r

A90: - J = partdiff`2 (f1,x1) by A51, A88

.= (f1 `partial`2| Z) /. x1 by A84, A88, NDIFF_7:def 11 ;

- J = partdiff`2 (f1,x0) by A51, A86

.= (f1 `partial`2| Z) /. x0 by A84, A86, NDIFF_7:def 11 ;

then ((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0) = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A90, RLVECT_1:15;

hence ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r by A86, NORMSP_0:def 6; :: thesis: verum

hence ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z ) by A9, A37, A50, A84, NDIFF_7:52; :: thesis: for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

thus for x being Point of E

for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) :: thesis: verum

proof

let x be Point of E; :: thesis: for y being Point of F

for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

let y be Point of F; :: thesis: for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

let z be Point of [:E,F:]; :: thesis: ( x in D & z = [x,y] implies ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) )

assume A92: ( x in D & z = [x,y] ) ; :: thesis: ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

then A93: z in Z by A5, ZFMISC_1:87;

take J ; :: thesis: ( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - J )

thus J = id the carrier of F ; :: thesis: ( partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - J )

thus partdiff`1 (f1,z) = diff (f,x) by A10, A92, A93; :: thesis: partdiff`2 (f1,z) = - J

thus partdiff`2 (f1,z) = - J by A51, A93; :: thesis: verum

end;for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

let y be Point of F; :: thesis: for z being Point of [:E,F:] st x in D & z = [x,y] holds

ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

let z be Point of [:E,F:]; :: thesis: ( x in D & z = [x,y] implies ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) )

assume A92: ( x in D & z = [x,y] ) ; :: thesis: ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st

( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I )

then A93: z in Z by A5, ZFMISC_1:87;

take J ; :: thesis: ( J = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - J )

thus J = id the carrier of F ; :: thesis: ( partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - J )

thus partdiff`1 (f1,z) = diff (f,x) by A10, A92, A93; :: thesis: partdiff`2 (f1,z) = - J

thus partdiff`2 (f1,z) = - J by A51, A93; :: thesis: verum