defpred S₁[ set ] means $1 in X;
deffunc H₁( Real) -> Real = diff f,$1;
consider F being PartFunc of REAL ,REAL such that
A2: ( ( for x being Real holds
( x in dom F iff S₁[x] ) ) & ( for x being Real st x in dom F holds
F . x = H₁(x) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = X & ( for x being Real st x in X holds
F . x = diff f,x ) )
for y being set st y in dom F holds
y in X by A2;
then A3: dom F c= X by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in X implies y in dom F )
assume A4: y in X ; :: thesis: y in dom F
X is Subset of REAL by A1, Th15;
hence y in dom F by A2, A4; :: thesis: verum

end;

then X c= dom F by TARSKI:def 3;
hence dom F = X by A3, XBOOLE_0:def 10; :: thesis: for x being Real st x in X holds
F . x = diff f,x

now

let x be Real; :: thesis: ( x in X implies F . x = diff f,x )
assume x in X ; :: thesis: F . x = diff f,x
then x in dom F by A2;
hence F . x = diff f,x by A2; :: thesis: verum

end;

hence for x being Real st x in X holds
F . x = diff f,x ; :: thesis: verum