deffunc H1( Real) -> Element of REAL n = diff (f,$1);
defpred S1[ set ] means $1 in X;
consider F0 being PartFunc of REAL,(REAL n) such that
A2: ( ( for x being Element of REAL holds
( x in dom F0 iff S1[x] ) ) & ( for x being Element of REAL st x in dom F0 holds
F0 . x = H1(x) ) ) from SEQ_1:sch 3();
 take F0 ; :: thesis: ( dom F0 = X & ( for x being Real st x in X holds
F0 . x = diff (f,x) ) )
now :: thesis: for y being object st y in X holds
y in dom F0
A3: X is Subset of REAL by A1, Th4;
let y be object ; :: thesis: ( y in X implies y in dom F0 )
assume y in X ; :: thesis: y in dom F0
hence y in dom F0 by A2, A3; :: thesis: verum
end;
then A4: X c= dom F0 ;
for y being object st y in dom F0 holds
y in X by A2;
then dom F0 c= X ;
hence dom F0 = X by A4, XBOOLE_0:def 10; :: thesis: for x being Real st x in X holds
F0 . x = diff (f,x)
now :: thesis: for x being Real st x in X holds
F0 . x = diff (f,x)
let x be Real; :: thesis: ( x in X implies F0 . x = diff (f,x) )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in X ; :: thesis: F0 . x = diff (f,x)
then A5: xx in dom F0 by A2;
thus F0 . x = F0 . xx
.= diff (f,x) by A2, A5 ; :: thesis: verum
end;
hence for x being Real st x in X holds
F0 . x = diff (f,x) ; :: thesis: verum