deffunc H_{1}( Element of REAL 2) -> Element of REAL = In ((partdiff (f,$1,1)),REAL);

defpred S_{1}[ Element of REAL 2] means $1 in Z;

consider F being PartFunc of (REAL 2),REAL such that

A2: ( ( for z being Element of REAL 2 holds

( z in dom F iff S_{1}[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds

F . z = H_{1}(z) ) )
from SEQ_1:sch 3();

take F ; :: thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1) ) )

for y being object st y in dom F holds

y in Z by A2;

then dom F c= Z ;

hence dom F = Z by A4, XBOOLE_0:def 10; :: thesis: for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1)

let z be Element of REAL 2; :: thesis: ( z in Z implies F . z = partdiff (f,z,1) )

assume z in Z ; :: thesis: F . z = partdiff (f,z,1)

then z in dom F by A2;

then F . z = H_{1}(z)
by A2;

hence F . z = partdiff (f,z,1) ; :: thesis: verum

defpred S

consider F being PartFunc of (REAL 2),REAL such that

A2: ( ( for z being Element of REAL 2 holds

( z in dom F iff S

F . z = H

take F ; :: thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1) ) )

now :: thesis: for y being object st y in Z holds

y in dom F

then A4:
Z c= dom F
;y in dom F

Z c= dom f
by A1;

then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;

let y be object ; :: thesis: ( y in Z implies y in dom F )

assume y in Z ; :: thesis: y in dom F

hence y in dom F by A2, A3; :: thesis: verum

end;then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;

let y be object ; :: thesis: ( y in Z implies y in dom F )

assume y in Z ; :: thesis: y in dom F

hence y in dom F by A2, A3; :: thesis: verum

for y being object st y in dom F holds

y in Z by A2;

then dom F c= Z ;

hence dom F = Z by A4, XBOOLE_0:def 10; :: thesis: for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1)

let z be Element of REAL 2; :: thesis: ( z in Z implies F . z = partdiff (f,z,1) )

assume z in Z ; :: thesis: F . z = partdiff (f,z,1)

then z in dom F by A2;

then F . z = H

hence F . z = partdiff (f,z,1) ; :: thesis: verum