let n be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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 )
( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) ;
reconsider y' = y as Point of (REAL-NS n) by REAL_NS1:def 4;
( h is_partial_differentiable_in y',i iff g1 is_partial_differentiable_in y,i ) by Th16;
hence ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) by A1, Th14; :: thesis: verum