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