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 b1 being Polynomial of L st
for x being Nat holds
( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) ) ; :: thesis: verum