deffunc H1( Element of REAL 2) -> Element of REAL = In ((partdiff (f,\$1,2)),REAL);
defpred S1[ 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 S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(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,2) ) )

now :: thesis: for y being object st y in Z holds
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 A4: Z c= dom F ;
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 ; :: thesis: for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2)

let z be Element of REAL 2; :: thesis: ( z in Z implies F . z = partdiff (f,z,2) )
assume z in Z ; :: thesis: F . z = partdiff (f,z,2)
then z in dom F by A2;
then F . z = H1(z) by A2;
hence F . z = partdiff (f,z,2) ; :: thesis: verum