let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m ex L being Lipschitzian 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 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); :: thesis: for x being Element of REAL m ex L being Lipschitzian 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 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; :: thesis: ex L being Lipschitzian 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 Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
defpred S₁[ set , set ] means ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being 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 S₁[v,y]

proof

let v be Element of REAL m; :: thesis: ex y being Element of REAL n st S₁[v,y]
defpred S₂[ set , set ] means ex i being 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 S₂[i,r]

proof

let i be Nat; :: thesis: ( i in Seg m implies ex r being Element of REAL n st S₂[i,r] )
assume i in Seg m ; :: thesis: ex r being Element of REAL n st S₂[i,r]
reconsider i0 = i as Nat ;
((proj (i0,m)) . v) * (partdiff (f,x,i0)) in REAL n ;
hence ex r being Element of REAL n st S₂[i,r] ; :: thesis: verum

end;

consider w being FinSequence of REAL n such that
A3: ( dom w = Seg m & ( for i being Nat st i in Seg m holds
S₂[i,w . i] ) ) from FINSEQ_1:sch 5(A2);

A4: now :: thesis: for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))

let i be Nat; :: thesis: ( i in Seg m implies w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) )
assume i in Seg m ; :: thesis: w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))
then S₂[i,w . i] by A3;
hence w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) ; :: thesis: 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 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 S₁[v,y0] ; :: thesis: verum

end;

consider L being Function of (REAL m),(REAL n) such that
A5: for h being Element of REAL m holds S₁[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; :: thesis: L . (s + t) = (L . s) + (L . t)
consider w being FinSequence of REAL n such that
A7: ( dom w = Seg m & ( for i being 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 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 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: w + v = w <++> v by INTEGR15:def 9;
A11: dom u = (dom w) /\ (dom v) by A7, A8, A9;

now :: thesis: for j being object st j in dom u holds
u . j = (w . j) + (v . j)

let j be object ; :: thesis: ( j in dom u implies u . j = (w . j) + (v . j) )
assume A12: j in dom u ; :: thesis: u . j = (w . j) + (v . j)
then reconsider i = j as Nat ;
A13: w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) by A7, A9, A12;
A14: v . i = ((proj (i,m)) . t) * (partdiff (f,x,i)) by A8, A9, A12;
thus u . j = ((proj (i,m)) . (s + t)) * (partdiff (f,x,i)) by A9, A12
.= ((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 A13, A14, RVSUM_1:50 ; :: thesis: verum

end;

then u = w + v by A10, A11, VALUED_2:def 45;
hence L . (s + t) = (L . s) + (L . t) by A9, A7, A8, Th24; :: thesis: 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; :: thesis: for r being Real holds L . (r * s) = r * (L . s)
let r be Real; :: thesis: L . (r * s) = r * (L . s)
consider w being FinSequence of REAL n such that
A15: ( dom w = Seg m & ( for i being 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 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;
A17: r (#) w = w [#] r by INTEGR15:def 11;

now :: thesis: for j being object st j in dom u holds
u . j = r (#) (w . j)

let j be object ; :: thesis: ( j in dom u implies u . j = r (#) (w . j) )
assume A18: j in dom u ; :: thesis: u . j = r (#) (w . j)
then reconsider i = j as Nat ;
A19: w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) by A15, A16, A18;
thus u . j = ((proj (i,m)) . (r * s)) * (partdiff (f,x,i)) by A16, A18
.= ((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 A19, RVSUM_1:49 ; :: thesis: verum

end;

then u = r (#) w by A17, A15, A16, VALUED_2:def 39;
hence L . (r * s) = r * (L . s) by A15, A16, Th25; :: thesis: verum

end;

then reconsider L = L as LinearOperator of m,n by A6, PDIFF_6:def 1, PDIFF_6:def 2;
take L ; :: thesis: for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being 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 Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w ) by A5; :: thesis: verum