let m, n be non empty Element of NAT ; :: thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff F,x = diff G,y
let F be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff F,x = diff G,y
let G be PartFunc of (REAL m),(REAL n); :: thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff F,x = diff G,y
let x be Point of (REAL-NS m); :: thesis: for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff F,x = diff G,y
let y be Element of REAL m; :: thesis: ( F = G & x = y & F is_differentiable_in x implies diff F,x = diff G,y )
assume A1: ( F = G & x = y & F is_differentiable_in x ) ; :: thesis: diff F,x = diff G,y
then A2: G is_differentiable_in y by Th20;
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then diff F,x is Function of (REAL m),(REAL n) by LOPBAN_1:def 10;
hence diff F,x = diff G,y by A1, A2, Def8; :: thesis: verum