let n be non zero Nat; :: thesis: for i being Nat
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let i be Nat; :: thesis: for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let g be PartFunc of (REAL n),REAL; :: thesis: for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let y be Element of REAL n; :: thesis: for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let g1 be PartFunc of (REAL n),(REAL 1); :: thesis: ( g1 = <>* g implies ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) )
assume A1: g1 = <>* g ; :: thesis: ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def 4;
( h is_partial_differentiable_in y9,i iff g1 is_partial_differentiable_in y,i ) ;
hence ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) by A1, Th14; :: thesis: verum