let N0 be Nat; :: thesis: for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
let F be FinSequence of the carrier of (Polynom-Ring (n,L)); :: thesis: for x being Function of n,L st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
let x be Function of n,L; :: thesis: ( len F = N0 + 1 implies E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*> )
assume A1: len F = N0 + 1 ; :: thesis: E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>
then A2: dom F = Seg (N0 + 1) by FINSEQ_1:def 3;
then A3: Seg (N0 + 1) = dom (E_eval (F,x)) by Def2
.= Seg (len (E_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 (E_eval ((F | N0),x))) = dom (E_eval ((F | N0),x)) by FINSEQ_1:def 3
.= dom (F | N0) by Def2
.= Seg N0 by A4, FINSEQ_1:def 3 ;
then A6: len (E_eval ((F | N0),x)) = N0 by FINSEQ_1:6;
len <*(E_eval ((F /. (N0 + 1)),x))*> = 1 by FINSEQ_1:39;
then A8: len ((E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (N0 + 1)),x))*>) = N0 + 1 by A6, FINSEQ_1:22;
for k being Nat st 1 <= k & k <= len (E_eval (F,x)) holds
(E_eval (F,x)) . k = ((E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>) . k

proof

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

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

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

then A14: k in dom (F | N0) by A4, FINSEQ_1:def 3;
then A15: k in dom (E_eval ((F | N0),x)) by Def2;
A16: k in dom (F | (Seg N0)) by A12, A4, FINSEQ_1:def 3;
A17: (F | N0) /. k = (F | (Seg N0)) . k by A14, PARTFUN1:def 6
.= F . k by A16, FUNCT_1:47
.= F /. k by A2, A12, A13, PARTFUN1:def 6 ;
((E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (N0 + 1)),x))*>) . k = (E_eval ((F | N0),x)) . k by A15, FINSEQ_1:def 7
.= E_eval ((F /. k),x) by A17, A14, Def2
.= (E_eval (F,x)) . k by Def2, A2, A12, A13 ;
hence (E_eval (F,x)) . k = ((E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>) . k by A1; :: thesis: verum

end;

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

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

end;

end;

end;

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