defpred S₁[ Element of REAL 3] means $1 in D;
deffunc H₁( Element of REAL 3) -> Element of REAL = In ((hpartdiff22 (f,$1)),REAL);
consider F being PartFunc of (REAL 3),REAL such that
A2: ( ( for u being Element of REAL 3 holds
( u in dom F iff S₁[u] ) ) & ( for u being Element of REAL 3 st u in dom F holds
F . u = H₁(u) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = hpartdiff22 (f,u) ) )
for y being object st y in dom F holds
y in D by A2;
then A3: dom F c= D by TARSKI:def 3;

now :: thesis: for y being object st y in D holds
y in dom F

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

end;

then D c= dom F by TARSKI:def 3;
hence dom F = D by A3; :: thesis: for u being Element of REAL 3 st u in D holds
F . u = hpartdiff22 (f,u)

hereby :: thesis: verum

let u be Element of REAL 3; :: thesis: ( u in D implies F . u = hpartdiff22 (f,u) )
assume u in D ; :: thesis: F . u = hpartdiff22 (f,u)
then u in dom F by A2;
hence F . u = H₁(u) by A2
.= hpartdiff22 (f,u) ;
:: thesis: verum

end;