set FuFF = Funcs (COMPLEX,COMPLEX);
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 )
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 ; :: 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
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 :: thesis: for u, v, w being Element of L holds (u + v) + w = u + (v + w)
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: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 ; :: thesis: verum
end;
A7: now :: thesis: for v being Element of L holds v + (0. L) = v
let v be Element of L; :: thesis: v + (0. L) = v
reconsider v1 = v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A8: now :: thesis: for x being Element of COMPLEX holds (v1 + fzero) . x = v1 . x
let x be Element of COMPLEX ; :: thesis: (v1 + fzero) . x = v1 . x
thus (v1 + fzero) . x = (v1 . x) + (fzero . x) by VALUED_1:1
.= (v1 . x) + 0c by FUNCOP_1:7
.= v1 . x ; :: thesis: verum
end;
thus v + (0. L) = v1 + fzero by A3
.= v by A8, FUNCT_2:63 ; :: thesis: verum
end;
L is right_complementable
proof
let v be Element of L; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
reconsider w = - v1 as Element of L by FUNCT_2:9;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. L
A9: now :: thesis: for x being Element of COMPLEX holds (v1 + (- v1)) . x = fzero . x
let x be Element of COMPLEX ; :: thesis: (v1 + (- v1)) . x = fzero . x
thus (v1 + (- v1)) . x = (v1 . x) + ((- v1) . x) by VALUED_1:1
.= (v1 . x) + (- (v1 . x)) by VALUED_1:8
.= fzero . x by FUNCOP_1:7 ; :: thesis: verum
end;
thus v + w = v1 + (- v1) by A3
.= 0. L by A9, FUNCT_2:63 ; :: thesis: verum
end;
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;
A10: now :: thesis: for n being Nat st n in Seg (len p) holds
ex x being Element of L st S1[n,x]
let n be Nat; :: thesis: ( n in Seg (len p) implies ex x being Element of L st S1[n,x] )
reconsider x = FPower ((p . (n -' 1)),(n -' 1)) as Element of L by A1, FUNCT_2:9;
assume n in Seg (len p) ; :: thesis: ex x being Element of L st S1[n,x]
take x = x; :: thesis: S1[n,x]
thus S1[n,x] ; :: thesis: verum
end;
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 :: thesis: for x being Element of COMPLEX holds f . x = SF . x
let x be Element of COMPLEX ; :: thesis: f . x = SF . x
reconsider 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; :: thesis: ( 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 ; :: thesis: S2[k + 1]
reconsider SFk1 = Sum (F | k) as Function of COMPLEX,COMPLEX by FUNCT_2:66;
let SFk be Function of COMPLEX,COMPLEX; :: thesis: ( SFk = Sum (F | (k + 1)) implies Sum (H | (k + 1)) = SFk . x )
assume A21: SFk = Sum (F | (k + 1)) ; :: thesis: Sum (H | (k + 1)) = SFk . x
per cases ( len F > k or len F <= k ) ;
suppose A22: len F > k ; :: thesis: Sum (H | (k + 1)) = SFk . x
reconsider 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 ;
:: thesis: verum
end;
suppose A30: len F <= k ; :: thesis: Sum (H | (k + 1)) = SFk . x
k <= k + 1 by NAT_1:11;
then A31: ( F | (k + 1) = F & H | (k + 1) = H ) by A16, A18, A30, FINSEQ_1:58, XXREAL_0:2;
( F | k = F & H | k = H ) by A16, A18, A30, FINSEQ_1:58;
hence Sum (H | (k + 1)) = SFk . x by A20, A21, A31; :: thesis: verum
end;
end;
end;
A32: S2[ 0 ]
proof
let SFk be Function of COMPLEX,COMPLEX; :: thesis: ( SFk = Sum (F | 0) implies Sum (H | 0) = SFk . x )
A33: F | 0 = <*> the carrier of L ;
assume SFk = Sum (F | 0) ; :: thesis: Sum (H | 0) = SFk . x
then A34: SFk = 0. L by A33, RLVECT_1:43
.= COMPLEX --> 0c ;
H | 0 = <*> the carrier of F_Complex ;
hence Sum (H | 0) = 0. F_Complex by RLVECT_1:43
.= SFk . x by A34, COMPLFLD:7, FUNCOP_1:7 ;
:: thesis: verum
end;
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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: S2[k + 1]
then A39: g1 is_continuous_on COMPLEX ;
let g be PartFunc of COMPLEX,COMPLEX; :: thesis: ( g = Sum (F | (k + 1)) implies g is_continuous_on COMPLEX )
assume A40: g = Sum (F | (k + 1)) ; :: thesis: g is_continuous_on COMPLEX
per cases ( len F > k or len F <= k ) ;
suppose A41: len F > k ; :: thesis: 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; :: thesis: verum
end;
end;
end;
A48: S2[ 0 ]
proof
let g be PartFunc of COMPLEX,COMPLEX; :: thesis: ( g = Sum (F | 0) implies g is_continuous_on COMPLEX )
A49: F | 0 = <*> the carrier of L ;
assume g = Sum (F | 0) ; :: thesis: g is_continuous_on COMPLEX
then g = 0. L by A49, RLVECT_1:43
.= COMPLEX --> 0c ;
hence g is_continuous_on COMPLEX by Th63; :: thesis: verum
end;
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; :: thesis: verum