let m, n be non empty Element of NAT ; for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m ex L being bounded LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
let f be PartFunc of (REAL m),(REAL n); for x being Element of REAL m ex L being bounded LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
let x be Element of REAL m; ex L being bounded LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
defpred S1[ set , set ] means ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . $1) * (partdiff (f,x,i)) ) & $2 = Sum w );
A1:
for v being Element of REAL m ex y being Element of REAL n st S1[v,y]
proof
let v be
Element of
REAL m;
ex y being Element of REAL n st S1[v,y]
defpred S2[
set ,
set ]
means ex
i being
Element of
NAT st
(
i = $1 & $2
= ((proj (i,m)) . v) * (partdiff (f,x,i)) );
A2:
for
i being
Nat st
i in Seg m holds
ex
r being
Element of
REAL n st
S2[
i,
r]
consider w being
FinSequence of
REAL n such that A3:
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
S2[
i,
w . i] ) )
from FINSEQ_1:sch 5(A2);
A4:
now let i be
Element of
NAT ;
( i in Seg m implies w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) )assume
i in Seg m
;
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))then
S2[
i,
w . i]
by A3;
hence
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))
;
verum end;
reconsider w0 =
Sum w as
Element of
REAL n ;
ex
w being
FinSequence of
REAL n st
(
dom w = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) ) &
w0 = Sum w )
by A4, A3;
hence
ex
y0 being
Element of
REAL n st
S1[
v,
y0]
;
verum
end;
consider L being Function of (REAL m),(REAL n) such that
A5:
for h being Element of REAL m holds S1[h,L . h]
from FUNCT_2:sch 3(A1);
A6:
for s, t being Element of REAL m holds L . (s + t) = (L . s) + (L . t)
proof
let s,
t be
Element of
REAL m;
L . (s + t) = (L . s) + (L . t)
consider w being
FinSequence of
REAL n such that A7:
(
dom w = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) ) &
L . s = Sum w )
by A5;
consider v being
FinSequence of
REAL n such that A8:
(
dom v = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
v . i = ((proj (i,m)) . t) * (partdiff (f,x,i)) ) &
L . t = Sum v )
by A5;
consider u being
FinSequence of
REAL n such that A9:
(
dom u = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
u . i = ((proj (i,m)) . (s + t)) * (partdiff (f,x,i)) ) &
L . (s + t) = Sum u )
by A5;
B1:
w + v = w <++> v
by INTEGR15:def 9;
A10:
dom u = (dom w) /\ (dom v)
by A7, A8, A9;
now let j be
set ;
( j in dom u implies u . j = (w . j) + (v . j) )assume A11:
j in dom u
;
u . j = (w . j) + (v . j)then reconsider i =
j as
Element of
NAT ;
A12:
( 1
<= i &
i <= m )
by A9, A11, FINSEQ_1:1;
B13:
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i))
by A7, A9, A11;
B14:
v . i = ((proj (i,m)) . t) * (partdiff (f,x,i))
by A8, A9, A11;
thus u . j =
((proj (i,m)) . (s + t)) * (partdiff (f,x,i))
by A9, A11
.=
((s + t) . i) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
((s . i) + (t . i)) * (partdiff (f,x,i))
by RVSUM_1:11
.=
(((proj (i,m)) . s) + (t . i)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(((proj (i,m)) . s) + ((proj (i,m)) . t)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(w . j) + (v . j)
by B13, B14, RVSUM_1:50
;
verum end;
then
u = w + v
by B1, A10, VALUED_2:def 45;
hence
L . (s + t) = (L . s) + (L . t)
by A9, A7, A8, Th24;
verum
end;
for s being Element of REAL m
for r being Real holds L . (r * s) = r * (L . s)
proof
let s be
Element of
REAL m;
for r being Real holds L . (r * s) = r * (L . s)let r be
Real;
L . (r * s) = r * (L . s)
consider w being
FinSequence of
REAL n such that A15:
(
dom w = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) ) &
L . s = Sum w )
by A5;
consider u being
FinSequence of
REAL n such that A16:
(
dom u = Seg m & ( for
i being
Element of
NAT st
i in Seg m holds
u . i = ((proj (i,m)) . (r * s)) * (partdiff (f,x,i)) ) &
L . (r * s) = Sum u )
by A5;
B1:
r (#) w = w [#] r
by INTEGR15:def 11;
now let j be
set ;
( j in dom u implies u . j = r (#) (w . j) )assume A17:
j in dom u
;
u . j = r (#) (w . j)then reconsider i =
j as
Element of
NAT ;
A18:
( 1
<= i &
i <= m )
by A16, A17, FINSEQ_1:1;
B19:
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i))
by A15, A16, A17;
thus u . j =
((proj (i,m)) . (r * s)) * (partdiff (f,x,i))
by A16, A17
.=
((r * s) . i) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(r * (s . i)) * (partdiff (f,x,i))
by RVSUM_1:45
.=
(r * ((proj (i,m)) . s)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
r (#) (w . j)
by B19, RVSUM_1:49
;
verum end;
then
u = r (#) w
by B1, A15, A16, VALUED_2:def 39;
hence
L . (r * s) = r * (L . s)
by A15, A16, Th25;
verum
end;
then reconsider L = L as LinearOperator of m,n by A6, PDIFF_6:def 1, PDIFF_6:def 2;
take
L
; for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
thus
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
by A5; verum