deffunc H₁( Real) -> Element of REAL = In ((diff (f,$1)),REAL);
defpred S₁[ set ] means $1 in X;
consider F being PartFunc of REAL,REAL such that
A2: ( ( for x being Element of REAL holds
( x in dom F iff S₁[x] ) ) & ( for x being Element of 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) ) )

now :: thesis: for y being object st y in X holds
y in dom F

A3: X is Subset of REAL by A1, Th8;
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 Real st x in X holds
F . x = diff (f,x)
for x being Real st x in X holds
F . x = diff (f,x)

proof

let x be Real; :: thesis: ( x in X implies F . x = diff (f,x) )
reconsider x = x as Element of REAL by XREAL_0:def 1;
( x in X implies F . x = H₁(x) ) by A2;
hence ( x in X implies F . x = diff (f,x) ) ; :: thesis: verum

end;

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