defpred S₁[ Element of REAL 2] means $1 in Z;
deffunc H₁( Element of REAL 2) -> Element of REAL = partdiff f,$1,1;
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₁[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H₁(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 set st y in dom F holds
y in Z by A2;
then A3: dom F c= Z by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in Z implies y in dom F )
assume A4: y in Z ; :: thesis: y in dom F
Z c= dom f by A1, Def16;
then Z is Subset of (REAL 2) by XBOOLE_1:1;
hence y in dom F by A2, A4; :: thesis: verum

end;

then Z c= dom F by TARSKI:def 3;
hence dom F = Z by A3, 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;
hence F . z = partdiff f,z,1 by A2; :: thesis: verum