defpred S1[ Element of REAL 3] means $1 in D;
deffunc H1( Element of REAL 3) -> Element of REAL = In ((partdiff (f,$1,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 S1[u] ) ) & ( for u being Element of REAL 3 st u in dom F holds
F . u = H1(u) ) )
from SEQ_1:sch 3();
take
F
; ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1) ) )
for y being object st y in dom F holds
y in D
by A2;
then A3:
dom F c= D
;
then
D c= dom F
;
hence
dom F = D
by A3; for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1)
let u be Element of REAL 3; ( u in D implies F . u = partdiff (f,u,1) )
assume
u in D
; F . u = partdiff (f,u,1)
then
u in dom F
by A2;
then
F . u = H1(u)
by A2;
hence
F . u = partdiff (f,u,1)
; verum