deffunc H₁( Element of (REAL-NS m)) -> Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) = partdiff f,$1,i;
defpred S₁[ 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 S₁[x] ) ) & ( for x being Point of (REAL-NS m) st x in dom F holds
F . x = H₁(x) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff f,x,i ) )

now

A3: X is Subset of (REAL-NS m) by A1, Th25;
let y be set ; :: thesis: ( y in X implies y in dom F )
assume y in X ; :: thesis: y in dom F
hence y in dom F by A2, A3; :: thesis: verum

end;

then A4: X c= dom F by TARSKI:def 3;
for y being set st y in dom F holds
y in X by A2;
then dom F c= X by TARSKI:def 3;
hence dom F = X by A4, XBOOLE_0:def 10; :: thesis: for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff f,x,i

hereby :: thesis: verum

let x be Point of (REAL-NS m); :: thesis: ( x in X implies F /. x = partdiff f,x,i )
assume x in X ; :: thesis: F /. x = partdiff f,x,i
then A5: x in dom F by A2;
then F . x = partdiff f,x,i by A2;
hence F /. x = partdiff f,x,i by A5, PARTFUN1:def 8; :: thesis: verum

end;