let n be non zero Nat; :: thesis: for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let i be Nat; :: thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let f be PartFunc of (REAL-NS n),(REAL-NS 1); :: thesis: for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let g be PartFunc of (REAL n),REAL; :: thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let y be Element of REAL n; :: thesis: ( f = <>* g & x = y implies ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) )
assume that
A1: f = <>* g and
A2: x = y ; :: thesis: ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
A3: <*((proj (i,n)) . y)*> = (Proj (i,n)) . x by A2, Def4;
f * (reproj (i,x)) = <>* (g * (reproj (i,y))) by A1, A2, Th13;
hence ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) by A3, Th7, Th8; :: thesis: verum