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

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