deffunc H_{1}( Real) -> Element of REAL n = diff (f,$1);

defpred S_{1}[ 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 S_{1}[x] ) ) & ( for x being Element of REAL st x in dom F0 holds

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

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)

F0 . x = diff (f,x) ; :: thesis: verum

defpred S

consider F0 being PartFunc of REAL,(REAL n) such that

A2: ( ( for x being Element of REAL holds

( x in dom F0 iff S

F0 . x = H

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

then A4:
X c= dom F0
;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;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

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)

hence
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;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

F0 . x = diff (f,x) ; :: thesis: verum