let N0 be Nat; :: thesis: for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L st len F = N0 + 1 holds
eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>
let L be comRing; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L st len F = N0 + 1 holds
eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>
let F be FinSequence of the carrier of (Polynom-Ring L); :: thesis: for x being Element of L st len F = N0 + 1 holds
eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>
let x be Element of L; :: thesis: ( len F = N0 + 1 implies eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*> )
assume A1: len F = N0 + 1 ; :: thesis: eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>
then A2: dom F = Seg (N0 + 1) by FINSEQ_1:def 3;
then A3: Seg (N0 + 1) = dom (eval (F,x)) by Def8
.= Seg (len (eval (F,x))) by FINSEQ_1:def 3 ;
A4: len (F | N0) = min (N0,(len F)) by FINSEQ_2:21
.= N0 by A1 ;
A5: Seg (len (eval ((F | N0),x))) = dom (eval ((F | N0),x)) by FINSEQ_1:def 3
.= dom (F | N0) by Def8
.= Seg N0 by A4, FINSEQ_1:def 3 ;
then A6: len (eval ((F | N0),x)) = N0 by FINSEQ_1:6;
len <*(eval ((~ (F /. (N0 + 1))),x))*> = 1 by FINSEQ_1:39;
then A7: len ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (N0 + 1))),x))*>) = N0 + 1 by A6, FINSEQ_1:22;
for k being Nat st 1 <= k & k <= len (eval (F,x)) holds
(eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (eval (F,x)) implies (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k )
assume ( 1 <= k & k <= len (eval (F,x)) ) ; :: thesis: (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k
then k in Seg (N0 + 1) by A3;
then A8: k in (Seg N0) \/ {(N0 + 1)} by FINSEQ_1:9;
A9: Seg N0 c= Seg (N0 + 1) by FINSEQ_3:18;

per cases ( k in Seg N0 or k in {(N0 + 1)} ) by A8, XBOOLE_0:def 3;

suppose A10: k in Seg N0 ; :: thesis: (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k

then A11: k in dom (F | N0) by A4, FINSEQ_1:def 3;
then A12: k in dom (eval ((F | N0),x)) by Def8;
A13: k in dom (F | (Seg N0)) by A10, A4, FINSEQ_1:def 3;
A14: (F | N0) /. k = (F | (Seg N0)) . k by A11, PARTFUN1:def 6
.= F . k by A13, FUNCT_1:47
.= F /. k by A2, A10, A9, PARTFUN1:def 6 ;
((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (N0 + 1))),x))*>) . k = (eval ((F | N0),x)) . k by A12, FINSEQ_1:def 7
.= eval ((~ (F /. k)),x) by A14, A11, Def8
.= (eval (F,x)) . k by Def8, A2, A10, A9 ;
hence (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k by A1; :: thesis: verum

end;

suppose k in {(N0 + 1)} ; :: thesis: (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k

then A15: k = N0 + 1 by TARSKI:def 1;
N0 + 1 = (len (eval ((F | N0),x))) + 1 by A5, FINSEQ_1:6;
hence (eval (F,x)) . k = ((eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) . k by A1, Def8, A2, FINSEQ_1:4, A15; :: thesis: verum

end;

end;

end;

hence eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*> by A1, A3, A7, FINSEQ_1:6; :: thesis: verum