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 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 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 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 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 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 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
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 ;
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. ) ) by ;
A16: dom (f - CST) = D /\ D by
.= D ;
A17: for s being object holds
( s in dom (f1 * ()) iff s in dom (f - CST) )
proof
let s be object ; :: thesis: ( s in dom (f1 * ()) iff s in dom (f - CST) )
hereby :: thesis: ( s in dom (f - CST) implies s in dom (f1 * ()) )
assume A19: s in dom (f1 * ()) ; :: thesis: s in dom (f - CST)
then reconsider t = s as Point of E ;
() . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then [t,y] in dom f1 by ;
hence s in dom (f - CST) by ; :: thesis: verum
end;
assume A20: s in dom (f - CST) ; :: thesis: s in dom (f1 * ())
then reconsider t = s as Point of E ;
() . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then A23: (reproj1 z) . t in dom f1 by ;
dom () = the carrier of E by FUNCT_2:def 1;
hence s in dom (f1 * ()) by ; :: thesis: verum
end;
A24: for s being object st s in dom (f1 * ()) holds
(f1 * ()) . s = (f - CST) . s
proof
let s be object ; :: thesis: ( s in dom (f1 * ()) implies (f1 * ()) . s = (f - CST) . s )
assume A25: s in dom (f1 * ()) ; :: thesis: (f1 * ()) . s = (f - CST) . s
then A26: ( s in dom () & () . s in dom f1 ) by FUNCT_1:11;
reconsider t = s as Point of E by A25;
A27: () . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then A28: t in D by ;
then A29: CST /. s = CST . s by
.= y by ;
thus (f1 * ()) . s = f1 . (t,y) by
.= (f /. t) - (CST /. s) by A7, A28, A29
.= (f - CST) /. s by
.= (f - CST) . s by ; :: thesis: verum
end;
A32: x in D by ;
then A33: f is_differentiable_in x by ;
CST is_differentiable_in x by ;
then A34: ( f - CST is_differentiable_in x & diff ((f - CST),x) = (diff (f,x)) - (diff (CST,x)) ) by ;
hence f1 is_partial_differentiable_in`1 z by ; :: thesis: partdiff`1 (f1,z) = diff (f,(z `1))
A36: diff (CST,x) = (CST `| D) /. x by
.= 0. by ;
thus partdiff`1 (f1,z) = diff ((f - CST),x) by
.= diff (f,(z `1)) by ; :: thesis: verum
end;
then A37: f1 is_partial_differentiable_on`1 Z by A6;
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
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 ;
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 ;
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 ;
- x0 = [(- s0),(- t0)] by ;
then x1 - x0 = [(s1 - s0),(t1 - t0)] by ;
then ||.(s1 - s0).|| <= ||.(x1 - x0).|| by LOPBAN_7:15;
then A48: ||.(s1 - s0).|| < s by ;
A49: (f `| D) /. s1 = diff (f,(x1 `1)) by
.= partdiff`1 (f1,x1) by
.= (f1 `partial`1| Z) /. x1 by ;
(f `| D) /. s0 = diff (f,(x0 `1)) by
.= partdiff`1 (f1,x0) by
.= (f1 `partial`1| Z) /. x0 by ;
hence ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r by A43, A46, A48, A49; :: thesis: verum
end;
then A50: f1 `partial`1| Z is_continuous_on Z by ;
reconsider J = FuncUnit F as Point of ;
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
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 )
proof
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;
then A53: CF is open by NDIFF_8:20;
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 ;
set fx = CF --> (f /. x);
A57: ( rng (CF --> (f /. x)) = {(f /. x)} & dom (CF --> (f /. x)) = CF ) by ;
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. ) ) by ;
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 ;
( 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 * ()) iff s in dom (fx - I) )
proof
let s be object ; :: thesis: ( s in dom (f1 * ()) iff s in dom (fx - I) )
A66: ( s in dom (f1 * ()) iff ( s in dom () & () . s in dom f1 ) ) by FUNCT_1:11;
thus ( s in dom (f1 * ()) implies s in dom (fx - I) ) by A63; :: thesis: ( s in dom (fx - I) implies s in dom (f1 * ()) )
assume s in dom (fx - I) ; :: thesis: s in dom (f1 * ())
then reconsider t = s as Point of F ;
A69: () . t = [(z `1),t] by NDIFF_7:def 2
.= [x,t] by A54 ;
dom () = the carrier of F by FUNCT_2:def 1;
hence s in dom (f1 * ()) by ; :: thesis: verum
end;
A71: for s being object st s in dom (f1 * ()) holds
(f1 * ()) . s = (fx - I) . s
proof
let s be object ; :: thesis: ( s in dom (f1 * ()) implies (f1 * ()) . s = (fx - I) . s )
assume A72: s in dom (f1 * ()) ; :: thesis: (f1 * ()) . s = (fx - I) . s
then reconsider t = s as Point of F ;
A73: () . t = [(z `1),t] by NDIFF_7:def 2
.= [x,t] by A54 ;
A74: t in CF ;
then A75: I /. s = I . s by
.= s by A74 ;
A76: fx /. s = fx . s by
.= f /. x by ;
thus (f1 * ()) . s = f1 . (x,t) by
.= (f /. x) - (I /. s) by A7, A55, A75
.= (fx - I) /. s by
.= (fx - I) . s by ; :: thesis: verum
end;
A79: fx is_differentiable_in y by ;
I is_differentiable_in y by ;
then A80: ( fx - I is_differentiable_in y & diff ((fx - I),y) = (diff (fx,y)) - (diff (I,y)) ) by ;
hence f1 is_partial_differentiable_in`2 z by ; :: thesis: partdiff`2 (f1,z) = - J
A82: diff (I,y) = (I `| CF) /. y by
.= J by ;
diff (fx,y) = (fx `| CF) /. y by
.= 0. by ;
then diff ((fx - I),y) = - J by ;
hence partdiff`2 (f1,z) = - J by ; :: thesis: verum
end;
then A84: f1 is_partial_differentiable_on`2 Z by A6;
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
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
.= (f1 `partial`2| Z) /. x1 by ;
- J = partdiff`2 (f1,x0) by
.= (f1 `partial`2| Z) /. x0 by ;
then ((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0) = 0. by ;
hence ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r by ; :: thesis: verum
end;
then f1 `partial`2| Z is_continuous_on Z by ;
hence ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z ) by ; :: 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 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 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 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 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 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 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 ;
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 ; :: thesis: partdiff`2 (f1,z) = - J
thus partdiff`2 (f1,z) = - J by ; :: thesis: verum
end;