deffunc H_{1}( Element of (REAL-NS m)) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) = partdiff (f,$1,i);

defpred S_{1}[ 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_{1}[x] ) ) & ( for x being Point of (REAL-NS m) st x in dom F holds

F . x = H_{1}(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) ) )

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; :: thesis: for x being Point of (REAL-NS m) st x in X holds

F /. x = partdiff (f,x,i)

defpred S

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

F . x = H

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 :: thesis: for y being object st y in X holds

y in dom F

then A4:
X c= dom F
;y in dom F

A3:
X is Subset of (REAL-NS m)
by A1, Th25;

let y be object ; :: 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;let y be object ; :: 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

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; :: 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 6; :: thesis: verum

end;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 6; :: thesis: verum