let m, n be non zero Nat; 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); 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); 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); 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; ( F = G & x = y & F is_differentiable_in x implies diff (F,x) = diff (G,y) )
assume that
A1:
F = G
and
A2:
x = y
and
A3:
F is_differentiable_in x
; diff (F,x) = diff (G,y)
A4:
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;
the carrier of (REAL-NS m) = REAL m
by REAL_NS1:def 4;
then A5:
diff (F,x) is Function of (REAL m),(REAL n)
by A4, LOPBAN_1:def 9;
G is_differentiable_in y
by A1, A2, A3;
hence
diff (F,x) = diff (G,y)
by A1, A2, A5, Def8; verum