let p be Polynomial of F_Complex ; :: thesis: ex f being Function of COMPLEX ,COMPLEX st
( f = Polynomial-Function F_Complex ,p & f is_continuous_on COMPLEX )
A1:
the carrier of F_Complex = COMPLEX
by COMPLFLD:def 1;
then reconsider f = Polynomial-Function F_Complex ,p as Function of COMPLEX ,COMPLEX ;
take
f
; :: thesis: ( f = Polynomial-Function F_Complex ,p & f is_continuous_on COMPLEX )
thus
f = Polynomial-Function F_Complex ,p
; :: thesis: f is_continuous_on COMPLEX
set FuFF = Funcs COMPLEX ,COMPLEX ;
deffunc H1( Element of Funcs COMPLEX ,COMPLEX , Element of Funcs COMPLEX ,COMPLEX ) -> Element of K30(K31(COMPLEX ,COMPLEX )) = $1 + $2;
A:
for x, y being Element of Funcs COMPLEX ,COMPLEX holds H1(x,y) in Funcs COMPLEX ,COMPLEX
by FUNCT_2:11;
consider fadd being BinOp of (Funcs COMPLEX ,COMPLEX ) such that
A2:
for x, y being Element of Funcs COMPLEX ,COMPLEX holds fadd . x,y = H1(x,y)
from FUNCT_7:sch 1(A);
reconsider fzero = COMPLEX --> 0c as Element of Funcs COMPLEX ,COMPLEX by FUNCT_2:12;
reconsider L = addLoopStr(# (Funcs COMPLEX ,COMPLEX ),fadd,fzero #) as non empty addLoopStr ;
A3:
now let u,
v,
w be
Element of
L;
:: thesis: (u + v) + w = u + (v + w)reconsider u1 =
u,
v1 =
v,
w1 =
w as
Function of
COMPLEX ,
COMPLEX by FUNCT_2:121;
A4:
(
u1 + v1 in Funcs COMPLEX ,
COMPLEX &
v1 + w1 in Funcs COMPLEX ,
COMPLEX )
by FUNCT_2:12;
thus (u + v) + w =
fadd . (u1 + v1),
w
by A2
.=
(u1 + v1) + w1
by A2, A4
.=
u1 + (v1 + w1)
by CFUNCT_1:22
.=
fadd . u,
(v1 + w1)
by A2, A4
.=
u + (v + w)
by A2
;
:: thesis: verum end;
L is right_complementable
then reconsider L = L as non empty right_complementable add-associative right_zeroed addLoopStr by A3, A5, RLVECT_1:def 6, RLVECT_1:def 7;
defpred S1[ Nat, set ] means $2 = FPower (p . ($1 -' 1)),($1 -' 1);
consider F being FinSequence of the carrier of L such that
A9:
dom F = Seg (len p)
and
A10:
for n being Nat st n in Seg (len p) holds
S1[n,F . n]
from FINSEQ_1:sch 5(A8);
A11:
F | (len F) = F
by FINSEQ_1:79;
defpred S2[ Element of NAT ] means for g being PartFunc of COMPLEX ,COMPLEX st g = Sum (F | $1) holds
g is_continuous_on COMPLEX ;
A12:
S2[ 0 ]
A14:
for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )
assume A15:
for
g being
PartFunc of
COMPLEX ,
COMPLEX st
g = Sum (F | k) holds
g is_continuous_on COMPLEX
;
:: thesis: S2[k + 1]
let g be
PartFunc of
COMPLEX ,
COMPLEX ;
:: thesis: ( g = Sum (F | (k + 1)) implies g is_continuous_on COMPLEX )
assume A16:
g = Sum (F | (k + 1))
;
:: thesis: g is_continuous_on COMPLEX
reconsider g1 =
Sum (F | k) as
Function of
COMPLEX ,
COMPLEX by FUNCT_2:121;
A17:
g1 is_continuous_on COMPLEX
by A15;
per cases
( len F > k or len F <= k )
;
suppose A18:
len F > k
;
:: thesis: g is_continuous_on COMPLEX then A19:
k + 1
<= len F
by NAT_1:13;
k + 1
>= 1
by NAT_1:11;
then A20:
k + 1
in dom F
by A19, FINSEQ_3:27;
then A21:
F /. (k + 1) =
F . (k + 1)
by PARTFUN1:def 8
.=
FPower (p . ((k + 1) -' 1)),
((k + 1) -' 1)
by A9, A10, A20
.=
FPower (p . k),
((k + 1) -' 1)
by NAT_D:34
.=
FPower (p . k),
k
by NAT_D:34
;
consider g2 being
Function of
COMPLEX ,
COMPLEX such that A22:
g2 = FPower (p . k),
k
and A23:
g2 is_continuous_on COMPLEX
by Th71;
F | (k + 1) =
(F | k) ^ <*(F . (k + 1))*>
by A18, POLYNOM3:19
.=
(F | k) ^ <*(F /. (k + 1))*>
by A20, PARTFUN1:def 8
;
then g =
(Sum (F | k)) + (F /. (k + 1))
by A16, FVSUM_1:87
.=
g1 + g2
by A2, A21, A22
;
hence
g is_continuous_on COMPLEX
by A17, A23, CFCONT_1:65;
:: thesis: verum end;
end;
A25:
for k being Element of NAT holds S2[k]
from NAT_1:sch 1(A12, A14);
reconsider SF = Sum F as Function of COMPLEX ,COMPLEX by FUNCT_2:121;
now let x be
Element of
COMPLEX ;
:: thesis: f . x = SF . xreconsider x1 =
x as
Element of
F_Complex by COMPLFLD:def 1;
consider H being
FinSequence of the
carrier of
F_Complex such that A26:
eval p,
x1 = Sum H
and A27:
len H = len p
and A28:
for
n being
Element of
NAT st
n in dom H holds
H . n = (p . (n -' 1)) * ((power F_Complex ) . x1,(n -' 1))
by POLYNOM4:def 2;
A29:
len F = len p
by A9, FINSEQ_1:def 3;
defpred S3[
Element of
NAT ]
means for
SFk being
Function of
COMPLEX ,
COMPLEX st
SFk = Sum (F | $1) holds
Sum (H | $1) = SFk . x;
A30:
S3[
0 ]
A33:
for
k being
Element of
NAT st
S3[
k] holds
S3[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S3[k] implies S3[k + 1] )
assume A34:
for
SFk being
Function of
COMPLEX ,
COMPLEX st
SFk = Sum (F | k) holds
Sum (H | k) = SFk . x
;
:: thesis: S3[k + 1]
let SFk be
Function of
COMPLEX ,
COMPLEX ;
:: thesis: ( SFk = Sum (F | (k + 1)) implies Sum (H | (k + 1)) = SFk . x )
assume A35:
SFk = Sum (F | (k + 1))
;
:: thesis: Sum (H | (k + 1)) = SFk . x
reconsider SFk1 =
Sum (F | k) as
Function of
COMPLEX ,
COMPLEX by FUNCT_2:121;
per cases
( len F > k or len F <= k )
;
suppose A36:
len F > k
;
:: thesis: Sum (H | (k + 1)) = SFk . xthen A37:
k + 1
<= len F
by NAT_1:13;
A38:
dom F = dom H
by A9, A27, FINSEQ_1:def 3;
k + 1
>= 1
by NAT_1:11;
then A39:
k + 1
in dom F
by A37, FINSEQ_3:27;
then A40:
H /. (k + 1) =
H . (k + 1)
by A38, PARTFUN1:def 8
.=
(p . ((k + 1) -' 1)) * ((power F_Complex ) . x1,((k + 1) -' 1))
by A28, A38, A39
.=
(p . k) * ((power F_Complex ) . x1,((k + 1) -' 1))
by NAT_D:34
.=
(p . k) * ((power F_Complex ) . x1,k)
by NAT_D:34
.=
(FPower (p . k),k) . x
by Def11
;
A41:
F /. (k + 1) =
F . (k + 1)
by A39, PARTFUN1:def 8
.=
FPower (p . ((k + 1) -' 1)),
((k + 1) -' 1)
by A9, A10, A39
.=
FPower (p . k),
((k + 1) -' 1)
by NAT_D:34
.=
FPower (p . k),
k
by NAT_D:34
;
reconsider g2 =
FPower (p . k),
k as
Function of
COMPLEX ,
COMPLEX by A1;
F | (k + 1) =
(F | k) ^ <*(F . (k + 1))*>
by A36, POLYNOM3:19
.=
(F | k) ^ <*(F /. (k + 1))*>
by A39, PARTFUN1:def 8
;
then A42:
SFk =
(Sum (F | k)) + (F /. (k + 1))
by A35, FVSUM_1:87
.=
SFk1 + g2
by A2, A41
;
A43:
Sum (H | k) = SFk1 . x
by A34;
H | (k + 1) =
(H | k) ^ <*(H . (k + 1))*>
by A27, A29, A36, POLYNOM3:19
.=
(H | k) ^ <*(H /. (k + 1))*>
by A38, A39, PARTFUN1:def 8
;
hence Sum (H | (k + 1)) =
(Sum (H | k)) + (H /. (k + 1))
by FVSUM_1:87
.=
SFk . x
by A40, A42, A43, VALUED_1:1
;
:: thesis: verum end;
end; A46:
for
k being
Element of
NAT holds
S3[
k]
from NAT_1:sch 1(A30, A33);
A47:
Sum (F | (len F)) = SF
by FINSEQ_1:79;
thus f . x =
Sum H
by A26, Def12
.=
Sum (H | (len H))
by FINSEQ_1:79
.=
SF . x
by A27, A29, A46, A47
;
:: thesis: verum end;
then
f = SF
by FUNCT_2:113;
hence
f is_continuous_on COMPLEX
by A11, A25; :: thesis: verum