let m, n be non zero Element of NAT ; :: thesis: for X being Subset of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS n) st X is open & X c= dom f holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
let X be Subset of (REAL-NS m); :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) st X is open & X c= dom f holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: ( X is open & X c= dom f implies ( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ) )
assume A1: ( X is open & X c= dom f ) ; :: thesis: ( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )

hereby :: thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ) implies ( f is_differentiable_on X & f `| X is_continuous_on X ) )

assume A2: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
let i, j be Nat; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= n implies ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
assume A3: ( 1 <= i & i <= m ) ; :: thesis: ( 1 <= j & j <= n implies ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
assume A4: ( 1 <= j & j <= n ) ; :: thesis: ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X )
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A1, A2, A3, PDIFF_8:22;
hence ( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by A1, A3, A4, PDIFF_8:20; :: thesis: verum

end;

assume A5: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) ; :: thesis: ( f is_differentiable_on X & f `| X is_continuous_on X )
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 )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A6: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) by A5;
hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A1, A6, PDIFF_8:20; :: thesis: verum

end;

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