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
; ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2) ) )
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 A4, XBOOLE_0:def 10; 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; ( z in Z implies F . z = partdiff (f,z,2) )
assume
z in Z
; 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)
; verum