let I be Function of REAL,(REAL 1); :: thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

let J be Function of (REAL 1),REAL; :: thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) )

assume that

A1: I = (proj (1,1)) " and

A2: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

thus for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc :: thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

let J be Function of (REAL 1),REAL; :: thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) )

assume that

A1: I = (proj (1,1)) " and

A2: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

thus for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc :: thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc

proof

thus
for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc
:: thesis: verum
let R be RestFunc of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * R) * I is RestFunc

A3: R is total by NDIFF_1:def 5;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider R0 = R as Function of (REAL 1),(REAL 1) by A3;

reconsider R1 = (J * R) * I as PartFunc of REAL,REAL ;

A4: (J * R0) * I is Function of REAL,REAL ;

then A5: dom R1 = REAL by FUNCT_2:def 1;

A6: for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

end;A3: R is total by NDIFF_1:def 5;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider R0 = R as Function of (REAL 1),(REAL 1) by A3;

reconsider R1 = (J * R) * I as PartFunc of REAL,REAL ;

A4: (J * R0) * I is Function of REAL,REAL ;

then A5: dom R1 = REAL by FUNCT_2:def 1;

A6: for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

proof

for h being non-zero 0 -convergent Real_Sequence holds
let r be Real; :: thesis: ( r > 0 implies ex d being Real st

( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) ) )

assume r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

then consider d being Real such that

A7: d > 0 and

A8: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds

(||.z.|| ") * ||.(R /. z).|| < r by A3, NDIFF_1:23;

take d ; :: thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r

(|.z1.| ") * |.(R1 . z1).| < r ) ) by A7; :: thesis: verum

end;( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) ) )

assume r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

then consider d being Real such that

A7: d > 0 and

A8: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds

(||.z.|| ") * ||.(R /. z).|| < r by A3, NDIFF_1:23;

take d ; :: thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r ) )

for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r

proof

hence
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
let z1 be Real; :: thesis: ( z1 <> 0 & |.z1.| < d implies (|.z1.| ") * |.(R1 . z1).| < r )

assume that

A9: z1 <> 0 and

A10: |.z1.| < d ; :: thesis: (|.z1.| ") * |.(R1 . z1).| < r

reconsider z1 = z1 as Element of REAL by XREAL_0:def 1;

reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def 4;

|.z1.| > 0 by A9, COMPLEX1:47;

then ||.z.|| <> 0 by A1, Th3;

then A11: z <> 0. (REAL-NS 1) ;

I * J = id (dom (proj (1,1))) by A1, A2, FUNCT_1:39;

then A12: I * J = id (REAL 1) by FUNCT_2:def 1;

A13: dom (J * R0) = REAL 1 by FUNCT_2:def 1;

R is total by NDIFF_1:def 5;

then A14: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

then R /. z = R . z by PARTFUN1:def 6;

then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:17;

then R /. z = ((I * J) * R) . (I . z1) by A12, REAL_NS1:def 4;

then A15: R /. z = (I * J) . (R . (I . z1)) by A14, FUNCT_1:13;

dom J = REAL 1 by FUNCT_2:def 1;

then R /. z = I . (J . (R0 . z)) by A15, FUNCT_1:13, FUNCT_2:5;

then R /. z = I . ((J * R0) . (I . z1)) by A13, FUNCT_1:12;

then R /. z = I . (R1 . z1) by A5, FUNCT_1:12;

then A16: ||.(R /. z).|| = |.(R1 . z1).| by A1, Th3;

A17: ||.z.|| " = |.z1.| " by A1, Th3;

||.z.|| < d by A1, A10, Th3;

hence (|.z1.| ") * |.(R1 . z1).| < r by A8, A11, A17, A16; :: thesis: verum

end;assume that

A9: z1 <> 0 and

A10: |.z1.| < d ; :: thesis: (|.z1.| ") * |.(R1 . z1).| < r

reconsider z1 = z1 as Element of REAL by XREAL_0:def 1;

reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def 4;

|.z1.| > 0 by A9, COMPLEX1:47;

then ||.z.|| <> 0 by A1, Th3;

then A11: z <> 0. (REAL-NS 1) ;

I * J = id (dom (proj (1,1))) by A1, A2, FUNCT_1:39;

then A12: I * J = id (REAL 1) by FUNCT_2:def 1;

A13: dom (J * R0) = REAL 1 by FUNCT_2:def 1;

R is total by NDIFF_1:def 5;

then A14: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

then R /. z = R . z by PARTFUN1:def 6;

then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:17;

then R /. z = ((I * J) * R) . (I . z1) by A12, REAL_NS1:def 4;

then A15: R /. z = (I * J) . (R . (I . z1)) by A14, FUNCT_1:13;

dom J = REAL 1 by FUNCT_2:def 1;

then R /. z = I . (J . (R0 . z)) by A15, FUNCT_1:13, FUNCT_2:5;

then R /. z = I . ((J * R0) . (I . z1)) by A13, FUNCT_1:12;

then R /. z = I . (R1 . z1) by A5, FUNCT_1:12;

then A16: ||.(R /. z).|| = |.(R1 . z1).| by A1, Th3;

A17: ||.z.|| " = |.z1.| " by A1, Th3;

||.z.|| < d by A1, A10, Th3;

hence (|.z1.| ") * |.(R1 . z1).| < r by A8, A11, A17, A16; :: thesis: verum

(|.z1.| ") * |.(R1 . z1).| < r ) ) by A7; :: thesis: verum

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

proof

hence
(J * R) * I is RestFunc
by A4, FDIFF_1:def 2; :: thesis: verum
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

hence lim ((h ") (#) (R1 /* h)) = 0 by A18, SEQ_2:def 7; :: thesis: verum

end;A18: now :: thesis: for r0 being Real st r0 > 0 holds

ex m being Nat st

for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

hence
(h ") (#) (R1 /* h) is convergent
by SEQ_2:def 6; :: thesis: lim ((h ") (#) (R1 /* h)) = 0 ex m being Nat st

for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

let r0 be Real; :: thesis: ( r0 > 0 implies ex m being Nat st

for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 )

reconsider r = r0 as Real ;

A19: lim h = 0 ;

assume r0 > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

then consider d being Real such that

A20: d > 0 and

A21: for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r by A6;

reconsider d1 = d as Real ;

consider m being Nat such that

A22: for n being Nat st m <= n holds

|.((h . n) - 0).| < d1 by A20, A19, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

end;for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 )

reconsider r = r0 as Real ;

A19: lim h = 0 ;

assume r0 > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

then consider d being Real such that

A20: d > 0 and

A21: for z1 being Real st z1 <> 0 & |.z1.| < d holds

(|.z1.| ") * |.(R1 . z1).| < r by A6;

reconsider d1 = d as Real ;

consider m being Nat such that

A22: for n being Nat st m <= n holds

|.((h . n) - 0).| < d1 by A20, A19, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st m <= n holds

|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

hereby :: thesis: verum

let n be Nat; :: thesis: ( m <= n implies |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 )

A23: h . n <> 0 by SEQ_1:5;

A24: n in NAT by ORDINAL1:def 12;

rng h c= dom R1 by A5;

then A25: (|.(h . n).| ") * |.(R1 . (h . n)).| = (|.(h . n).| ") * |.((R1 /* h) . n).| by FUNCT_2:108, A24

.= (((abs h) . n) ") * |.((R1 /* h) . n).| by SEQ_1:12

.= (((abs h) ") . n) * |.((R1 /* h) . n).| by VALUED_1:10

.= ((abs (h ")) . n) * |.((R1 /* h) . n).| by SEQ_1:54

.= |.((h ") . n).| * |.((R1 /* h) . n).| by SEQ_1:12

.= |.(((h ") . n) * ((R1 /* h) . n)).| by COMPLEX1:65

.= |.((((h ") (#) (R1 /* h)) . n) - 0).| by SEQ_1:8 ;

assume m <= n ; :: thesis: |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

then |.((h . n) - 0).| < d by A22;

hence |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 by A21, A23, A25; :: thesis: verum

end;A23: h . n <> 0 by SEQ_1:5;

A24: n in NAT by ORDINAL1:def 12;

rng h c= dom R1 by A5;

then A25: (|.(h . n).| ") * |.(R1 . (h . n)).| = (|.(h . n).| ") * |.((R1 /* h) . n).| by FUNCT_2:108, A24

.= (((abs h) . n) ") * |.((R1 /* h) . n).| by SEQ_1:12

.= (((abs h) ") . n) * |.((R1 /* h) . n).| by VALUED_1:10

.= ((abs (h ")) . n) * |.((R1 /* h) . n).| by SEQ_1:54

.= |.((h ") . n).| * |.((R1 /* h) . n).| by SEQ_1:12

.= |.(((h ") . n) * ((R1 /* h) . n)).| by COMPLEX1:65

.= |.((((h ") (#) (R1 /* h)) . n) - 0).| by SEQ_1:8 ;

assume m <= n ; :: thesis: |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

then |.((h . n) - 0).| < d by A22;

hence |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 by A21, A23, A25; :: thesis: verum

hence lim ((h ") (#) (R1 /* h)) = 0 by A18, SEQ_2:def 7; :: thesis: verum

proof

let L be LinearOperator of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * L) * I is LinearFunc

A26: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider L0 = L as Function of (REAL 1),(REAL 1) ;

reconsider L1 = (J * L0) * I as PartFunc of REAL,REAL ;

A27: dom (J * L0) = REAL 1 by FUNCT_2:def 1;

consider r being Real such that

A28: r = L1 . 1 ;

A29: dom ((J * L0) * I) = REAL by FUNCT_2:def 1;

A30: dom L0 = REAL 1 by FUNCT_2:def 1;

for p being Real holds L1 . p = r * p

end;A26: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider L0 = L as Function of (REAL 1),(REAL 1) ;

reconsider L1 = (J * L0) * I as PartFunc of REAL,REAL ;

A27: dom (J * L0) = REAL 1 by FUNCT_2:def 1;

consider r being Real such that

A28: r = L1 . 1 ;

A29: dom ((J * L0) * I) = REAL by FUNCT_2:def 1;

A30: dom L0 = REAL 1 by FUNCT_2:def 1;

for p being Real holds L1 . p = r * p

proof

hence
(J * L) * I is LinearFunc
by FDIFF_1:def 3; :: thesis: verum
reconsider 1p = I . jj as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;

let p be Real; :: thesis: L1 . p = r * p

reconsider pp = p, jj = 1 as Element of REAL by XREAL_0:def 1;

dom I = REAL by FUNCT_2:def 1;

then L1 . p = (J * L) . (I . (pp * jj)) by FUNCT_1:13;

then L1 . p = (J * L) . (p * 1p) by A1, Th3;

then L1 . p = J . (L . (p * 1p)) by A26, A30, FUNCT_1:13;

then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def 5;

then L1 . p = p * (J . (L . 1p)) by A2, Th4;

then L1 . p = p * ((J * L0) . (I . jj)) by A27, FUNCT_1:12;

hence L1 . p = r * p by A29, A28, FUNCT_1:12; :: thesis: verum

end;let p be Real; :: thesis: L1 . p = r * p

reconsider pp = p, jj = 1 as Element of REAL by XREAL_0:def 1;

dom I = REAL by FUNCT_2:def 1;

then L1 . p = (J * L) . (I . (pp * jj)) by FUNCT_1:13;

then L1 . p = (J * L) . (p * 1p) by A1, Th3;

then L1 . p = J . (L . (p * 1p)) by A26, A30, FUNCT_1:13;

then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def 5;

then L1 . p = p * (J . (L . 1p)) by A2, Th4;

then L1 . p = p * ((J * L0) . (I . jj)) by A27, FUNCT_1:12;

hence L1 . p = r * p by A29, A28, FUNCT_1:12; :: thesis: verum