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:9;
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 K1(K2(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:8;
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 for u, v, w being Element of L holds (u + v) + w = u + (v + w)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:66;
A5:
u1 + v1 in Funcs (
COMPLEX,
COMPLEX)
by FUNCT_2:9;
A6:
v1 + w1 in Funcs (
COMPLEX,
COMPLEX)
by FUNCT_2:9;
thus (u + v) + w =
fadd . (
(u1 + v1),
w)
by A3
.=
(u1 + v1) + w1
by A3, A5
.=
u1 + (v1 + w1)
by CFUNCT_1:13
.=
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 3, RLVECT_1:def 4;
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:58;
reconsider SF = Sum F as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A14:
now for x being Element of COMPLEX holds f . x = SF . xlet 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[
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
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
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:66;
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 . kk),
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:25;
then A25:
F /. (k + 1) =
F . (k + 1)
by PARTFUN1:def 6
.=
FPower (
(p . ((k + 1) -' 1)),
((k + 1) -' 1))
by A11, A12, A24
.=
FPower (
(p . kk),
((k + 1) -' 1))
by NAT_D:34
.=
FPower (
(p . kk),
k)
by NAT_D:34
;
F | (k + 1) =
(F | k) ^ <*(F . (k + 1))*>
by A22, FINSEQ_5:83
.=
(F | k) ^ <*(F /. (k + 1))*>
by A24, PARTFUN1:def 6
;
then A26:
SFk =
(Sum (F | k)) + (F /. (k + 1))
by A21, FVSUM_1:71
.=
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 6
.=
(p . ((k + 1) -' 1)) * ((power F_Complex) . (x1,((k + 1) -' 1)))
by A17, A28, A24
.=
(p . kk) * ((power F_Complex) . (x1,((k + 1) -' 1)))
by NAT_D:34
.=
(p . kk) * (power (x1,k))
by NAT_D:34
.=
(FPower ((p . kk),k)) . x
by Def12
;
H | (k + 1) =
(H | k) ^ <*(H . (k + 1))*>
by A16, A18, A22, FINSEQ_5:83
.=
(H | k) ^ <*(H /. (k + 1))*>
by A28, A24, PARTFUN1:def 6
;
hence Sum (H | (k + 1)) =
(Sum (H | k)) + (H /. (k + 1))
by FVSUM_1:71
.=
SFk . x
by A29, A26, A27, VALUED_1:1
;
verum end; end;
end; A32:
S2[
0 ]
A35:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A32, A19);
A36:
Sum (F | (len F)) = SF
by FINSEQ_1:58;
thus f . x =
Sum H
by A15, Def13
.=
Sum (H | (len H))
by FINSEQ_1:58
.=
SF . x
by A16, A18, A35, A36
;
verum end;
defpred S2[ Nat] means for g being PartFunc of COMPLEX,COMPLEX st g = Sum (F | $1) holds
g is_continuous_on COMPLEX ;
A37:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
reconsider g1 =
Sum (F | k) as
Function of
COMPLEX,
COMPLEX by FUNCT_2:66;
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:25;
then A44:
F /. (k + 1) =
F . (k + 1)
by PARTFUN1:def 6
.=
FPower (
(p . ((k + 1) -' 1)),
((k + 1) -' 1))
by A11, A12, A43
.=
FPower (
(p . kk),
((k + 1) -' 1))
by NAT_D:34
.=
FPower (
(p . kk),
k)
by NAT_D:34
;
consider g2 being
Function of
COMPLEX,
COMPLEX such that A45:
g2 = FPower (
(p . kk),
k)
and A46:
g2 is_continuous_on COMPLEX
by Th70;
F | (k + 1) =
(F | k) ^ <*(F . (k + 1))*>
by A41, FINSEQ_5:83
.=
(F | k) ^ <*(F /. (k + 1))*>
by A43, PARTFUN1:def 6
;
then g =
(Sum (F | k)) + (F /. (k + 1))
by A40, FVSUM_1:71
.=
g1 + g2
by A3, A44, A45
;
hence
g is_continuous_on COMPLEX
by A39, A46, CFCONT_1:43;
verum end; end;
end;
A48:
S2[ 0 ]
for k being Nat holds S2[k]
from NAT_1:sch 2(A48, A37);
hence
f is_continuous_on COMPLEX
by A13, A14, FUNCT_2:63; verum