let k be Nat; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len F = k + 1 holds
^ (F | k) = (^ F) | k
let F be FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len F = k + 1 implies ^ (F | k) = (^ F) | k )
set PRI = Polynom-Ring INT.Ring;
assume A1: len F = k + 1 ; :: thesis: ^ (F | k) = (^ F) | k
reconsider Fk = F | k as FinSequence of the carrier of (Polynom-Ring INT.Ring) ;
A2: k < k + 1 by NAT_1:13;
k <= len F by A1, NAT_1:13;
then len (F | k) = k by FINSEQ_1:59;
then A3: dom (F | k) = Seg k by FINSEQ_1:def 3;
A4: Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (^ F) by Def7
.= Seg (len (^ F)) by FINSEQ_1:def 3 ;
k <= len (^ F) by A2, A1, A4, FINSEQ_1:6;
then len ((^ F) | k) = k by FINSEQ_1:59;
then A5: dom ((^ F) | k) = Seg k by FINSEQ_1:def 3
.= dom (^ (F | k)) by Def7, A3 ;
for i being Nat st i in dom (^ (F | k)) holds
(^ (F | k)) . i = ((^ F) | k) . i

proof

let i be Nat; :: thesis: ( i in dom (^ (F | k)) implies (^ (F | k)) . i = ((^ F) | k) . i )
assume A6: i in dom (^ (F | k)) ; :: thesis: (^ (F | k)) . i = ((^ F) | k) . i
then A7: i in dom (F | k) by Def7;
A8: i in Seg k by A3, A6, Def7;
then ( 1 <= i & i <= k ) by FINSEQ_1:1;
then ( 1 <= i & i <= k + 1 ) by NAT_1:13;
then i in Seg (k + 1) ;
then A9: i in dom F by A1, FINSEQ_1:def 3;
then reconsider Fi = F . i as Element of the carrier of (Polynom-Ring INT.Ring) by FINSEQ_2:11;
A10: Fk /. i = (F | k) . i by A7, PARTFUN1:def 6
.= F . i by A8, FUNCT_1:49 ;
A11: F /. i = Fi by A9, PARTFUN1:def 6;
((^ F) | k) . i = (^ F) . i by A8, FUNCT_1:49
.= ^ Fi by A11, A9, Def7 ;
hence (^ (F | k)) . i = ((^ F) | k) . i by A10, Def7, A7; :: thesis: verum

end;

hence ^ (F | k) = (^ F) | k by A5; :: thesis: verum