defpred S₁[ Element of REAL m, set ] means ( $1 in Z & $2 = diff (f,$1) );
consider F being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) such that
A2: ( ( for x being Element of REAL m holds
( x in dom F iff ex z being Element of Funcs ((REAL m),REAL) st S₁[x,z] ) ) & ( for x being Element of REAL m st x in dom F holds
S₁[x,F . x] ) ) from SEQ_1:sch 2();
take F ; :: thesis: ( dom F = Z & ( for x being Element of REAL m st x in Z holds
F /. x = diff (f,x) ) )
A3: Z is Subset of (REAL m) by AK, XBOOLE_1:1;

now :: thesis: for x being set st x in Z holds
x in dom F

let x be set ; :: thesis: ( x in Z implies x in dom F )
assume AS1: x in Z ; :: thesis: x in dom F
then reconsider z = x as Element of REAL m by A3;
reconsider y = diff (f,z) as Element of Funcs ((REAL m),REAL) by FUNCT_2:8;
S₁[z,y] by AS1;
hence x in dom F by A2; :: thesis: verum

end;

then A4: Z c= dom F by TARSKI:def 3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def 3;
hence dom F = Z by A4, XBOOLE_0:def 10; :: thesis: for x being Element of REAL m st x in Z holds
F /. x = diff (f,x)

hereby :: thesis: verum

let x be Element of REAL m; :: thesis: ( x in Z implies F /. x = diff (f,x) )
assume A5: x in Z ; :: thesis: F /. x = diff (f,x)
then F . x = diff (f,x) by A2, A4;
hence F /. x = diff (f,x) by A5, A4, PARTFUN1:def 6; :: thesis: verum

end;