let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m st f is_differentiable_in x holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j )
assume A1: f is_differentiable_in x ; :: thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j
let i, j be Nat; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= n implies f is_partial_differentiable_in x,i,j )
assume A2: ( 1 <= i & i <= m ) ; :: thesis: ( not 1 <= j or not j <= n or f is_partial_differentiable_in x,i,j )
assume ( 1 <= j & j <= n ) ; :: thesis: f is_partial_differentiable_in x,i,j
then consider fj being PartFunc of (REAL m),REAL such that
A4: ( fj = (proj (j,n)) * f & fj is_differentiable_in x ) by A1, Th19;
fj is_partial_differentiable_in x,i by A2, A4, PDIFF_7:23;
hence f is_partial_differentiable_in x,i,j by A4; :: thesis: verum