deffunc H1( Element of (REAL-NS m)) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) = partdiff (f,$1,i);
defpred S1[ Element of (REAL-NS m)] means $1 in X;
consider F being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) such that
A2:
( ( for x being Point of (REAL-NS m) holds
( x in dom F iff S1[x] ) ) & ( for x being Point of (REAL-NS m) st x in dom F holds
F . x = H1(x) ) )
from SEQ_1:sch 3();
take
F
; ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i) ) )
then A4:
X c= dom F
;
for y being object st y in dom F holds
y in X
by A2;
then
dom F c= X
;
hence
dom F = X
by A4, XBOOLE_0:def 10; for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i)