let m, n be non zero Element of NAT ; :: thesis:
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis:
let X be Subset of (REAL-NS m); :: thesis:
assume A1: X is open ; :: thesis:

hereby :: thesis:

assume A2: for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis:

let j be Nat; :: thesis:
assume A3: ( 1 <= j & j <= n ) ; :: thesis:

let i be Nat; :: thesis:
assume A4: ( 1 <= i & i <= m ) ; :: thesis:
then ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A2;
hence ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by Th20, A1, A3, A4; :: thesis:

end;

hence ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) by A1, PDIFF_7:49; :: thesis:

end;

hence ( f is_differentiable_on X & f `| X is_continuous_on X ) by A1, Th21; :: thesis:

end;

assume A5: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis:
let i be Nat; :: thesis:
assume A6: ( 1 <= i & i <= m ) ; :: thesis:

let j be Nat; :: thesis:
assume ( 1 <= j & j <= n ) ; :: thesis:
then ( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) by A1, A5, Th21;
hence ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by A1, A6, PDIFF_7:49; :: thesis:

end;

hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A6, A1, Th20; :: thesis: