deffunc H₁( Element of [:X,Y:]) -> Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) = partdiff`1 (f,$1);
defpred S<sub>1</sub>[ set ] means $1 in Z;
consider F being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) such that
A3: ( ( for z being Point of [:X,Y:] holds
( z in dom F iff S<sub>1</sub>[z] ) ) & ( for z being Point of [:X,Y:] st z in dom F holds
F . z = H<sub>1</sub>(z) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = Z & ( for z being Point of [:X,Y:] st z in Z holds
F /. z = partdiff`1 (f,z) ) )

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

A4: Z is Subset of [:X,Y:] by A2, 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 A3, A4; :: thesis: verum

end;

then A5: Z c= dom F ;
dom F c= Z by A3;
hence dom F = Z by A5, XBOOLE_0:def 10; :: thesis: for z being Point of [:X,Y:] st z in Z holds
F /. z = partdiff`1 (f,z)

hereby :: thesis: verum

let x be Point of [:X,Y:]; :: thesis: ( x in Z implies F /. x = partdiff`1 (f,x) )
assume A6: x in Z ; :: thesis: F /. x = partdiff`1 (f,x)
then F . x = partdiff`1 (f,x) by A3;
hence F /. x = partdiff`1 (f,x) by A3, A6, PARTFUN1:def 6; :: thesis: verum

end;