deffunc H₁( Element of REAL m) -> Element of REAL = In ((partdiff (f,$1,i)),REAL);
defpred S₁[ Element of REAL m] means $1 in Z;
consider F being PartFunc of (REAL m),REAL such that
A2: ( ( for x being Element of REAL m holds
( x in dom F iff S₁[x] ) ) & ( for x being Element of REAL m st x in dom F holds
F . x = H₁(x) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = Z & ( for x being Element of REAL m st x in Z holds
F /. x = partdiff (f,x,i) ) )

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

A3: Z is Subset of (REAL m) by A1, XBOOLE_1:1;
let y be object ; :: thesis: ( y in Z implies y in dom F )
assume y in Z ; :: thesis: y in dom F
hence y in dom F by A2, A3; :: thesis: verum

end;

then A4: Z c= dom F ;
dom F c= Z by A2;
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 = partdiff (f,x,i)

hereby :: thesis: verum

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

end;