deffunc H1( Point of S) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) = diff (f,$1);
defpred S1[ Point of S] means $1 in X;
consider F being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) such that
A2: ( ( for x being Point of S holds
( x in dom F iff S1[x] ) ) & ( for x being Point of S st x in dom F holds
F . x = H1(x) ) ) from SEQ_1:sch 3();
 take F ; :: thesis: ( dom F = X & ( for x being Point of S st x in X holds
F /. x = diff (f,x) ) )
now :: thesis: for y being object st y in X holds
y in dom F
A3: X is Subset of S by A1, Th30;
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;
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; :: thesis: for x being Point of S st x in X holds
F /. x = diff (f,x)
now :: thesis: for x being Point of S st x in X holds
F /. x = diff (f,x)
let x be Point of S; :: thesis: ( x in X implies F /. x = diff (f,x) )
assume x in X ; :: thesis: F /. x = diff (f,x)
then A5: x in dom F by A2;
then F . x = diff (f,x) by A2;
hence F /. x = diff (f,x) by A5, PARTFUN1:def 6; :: thesis: verum
end;
hence for x being Point of S st x in X holds
F /. x = diff (f,x) ; :: thesis: verum