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;
A10:
dom u = (dom w) /\ (dom v)
by A7, A8, A9;
now let i be
Element of
NAT ;
( i in dom u implies u /. i = (w /. i) + (v /. i) )assume A11:
i in dom u
;
u /. i = (w /. i) + (v /. i)then A12:
( 1
<= i &
i <= m )
by A9, FINSEQ_1:3;
len w = m
by FINSEQ_1:def 3, A7;
then A13:
w /. i =
w . i
by A12, FINSEQ_4:24
.=
((proj (i,m)) . s) * (partdiff (f,x,i))
by A7, A9, A11
;
len v = m
by FINSEQ_1:def 3, A8;
then A14:
v /. i =
v . i
by A12, FINSEQ_4:24
.=
((proj (i,m)) . t) * (partdiff (f,x,i))
by A8, A9, A11
;
len u = m
by FINSEQ_1:def 3, A9;
hence u /. i =
u . i
by A12, FINSEQ_4:24
.=
((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:27
.=
(((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 /. i) + (v /. i)
by A13, A14, RVSUM_1:72
;
verum end;
then
u = w + v
by A10, INTEGR15:def 9;
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;
now let i be
Element of
NAT ;
( i in dom u implies u /. i = r * (w /. i) )assume A17:
i in dom u
;
u /. i = r * (w /. i)then A18:
( 1
<= i &
i <= m )
by A16, FINSEQ_1:3;
len w = m
by FINSEQ_1:def 3, A15;
then A19:
w /. i =
w . i
by A18, FINSEQ_4:24
.=
((proj (i,m)) . s) * (partdiff (f,x,i))
by A15, A16, A17
;
len u = m
by FINSEQ_1:def 3, A16;
hence u /. i =
u . i
by A18, FINSEQ_4:24
.=
((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:67
.=
(r * ((proj (i,m)) . s)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
r * (w /. i)
by A19, RVSUM_1:71
;
verum end;
then
u = r (#) w
by A15, A16, INTEGR15:def 11;
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