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

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

A4: X is Subset of (product G) by A2, XBOOLE_1:1;
let y be object ; :: thesis: ( y in X implies y in dom F )
assume y in X ; :: thesis: y in dom F
hence y in dom F by A3, A4; :: thesis: verum

end;

then A5: X c= dom F ;
dom F c= X by A3;
hence dom F = X by A5, XBOOLE_0:def 10; :: thesis: for x being Point of (product G) st x in X holds
F /. x = partdiff (f,x,i)

hereby :: thesis: verum

let x be Point of (product G); :: thesis: ( x in X implies F /. x = partdiff (f,x,i) )
assume A6: x in X ; :: thesis: F /. x = partdiff (f,x,i)
then F . x = partdiff (f,x,i) by A3;
hence F /. x = partdiff (f,x,i) by A3, A6, PARTFUN1:def 6; :: thesis: verum

end;