deffunc H1( Element of (product G)) -> Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) = partdiff (f,$1,i);
defpred S1[ 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 S1[x] ) ) & ( for x being Point of (product G) st x in dom F holds
F . x = H1(x) ) )
from SEQ_1:sch 3();
take
F
; ( dom F = X & ( for x being Point of (product G) st x in X holds
F /. x = partdiff (f,x,i) ) )
then A5:
X c= dom F
;
dom F c= X
by A3;
hence
dom F = X
by A5, XBOOLE_0:def 10; for x being Point of (product G) st x in X holds
F /. x = partdiff (f,x,i)
hereby verum
let x be
Point of
(product G);
( x in X implies F /. x = partdiff (f,x,i) )assume A6:
x in X
;
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;
verum
end;