reconsider x = (0_. L) +* (n,a) as sequence of L ;

now :: thesis: for i being Nat st i >= n + 1 holds
x . i = 0. L

let i be Nat; :: thesis: ( i >= n + 1 implies x . i = 0. L )
A1: i in NAT by ORDINAL1:def 12;
assume i >= n + 1 ; :: thesis: x . i = 0. L
then i > n by NAT_1:13;
hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum

end;

then reconsider x = x as Polynomial of L by ALGSEQ_1:def 1;

now :: thesis: for i being Nat holds
( ( i = n implies x . i = a ) & ( i <> n implies x . i = 0. L ) )

let i be Nat; :: thesis: ( ( i = n implies x . i = a ) & ( i <> n implies x . i = 0. L ) )
A2: i in NAT by ORDINAL1:def 12;
thus ( i = n implies x . i = a ) :: thesis: ( i <> n implies x . i = 0. L )

proof

A3: dom (0_. L) = NAT ;
assume i = n ; :: thesis: x . i = a
hence x . i = a by A2, A3, FUNCT_7:31; :: thesis: verum

end;

thus ( i <> n implies x . i = 0. L ) :: thesis: verum

proof

assume i <> n ; :: thesis: x . i = 0. L
hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32
.= 0. L by A2, FUNCOP_1:7 ;
:: thesis: verum

end;

end;

hence ex b₁ being Polynomial of L st
for x being Nat holds
( ( x = n implies b₁ . x = a ) & ( x <> n implies b₁ . x = 0. L ) ) ; :: thesis: verum