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 A1, XBOOLE_1:1;

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

let x be object ; :: thesis: ( x in Z implies x in dom F )
assume A4: 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 A4;
hence x in dom F by A2; :: thesis: verum

end;

then A5: Z c= dom F ;
dom F c= Z by A2;
hence dom F = Z by A5, 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 A6: x in Z ; :: thesis: F /. x = diff (f,x)
then F . x = diff (f,x) by A2, A5;
hence F /. x = diff (f,x) by A6, a5, PARTFUN1:def 6; :: thesis: verum

end;