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

_{1} being Polynomial of L st

for x being Nat holds

( ( x = n implies b_{1} . x = a ) & ( x <> n implies b_{1} . x = 0. L ) )
; :: thesis: verum

now :: thesis: for i being Nat st i >= n + 1 holds

x . i = 0. L

then reconsider x = x as Polynomial of L by ALGSEQ_1:def 1;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;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

now :: thesis: for i being Nat holds

( ( i = n implies x . i = a ) & ( i <> n implies x . i = 0. L ) )

hence
ex b( ( 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 )

end;A2: i in NAT by ORDINAL1:def 12;

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

proof

thus
( i <> n implies x . i = 0. L )
:: thesis: verum
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;assume i = n ; :: thesis: x . i = a

hence x . i = a by A2, A3, FUNCT_7:31; :: 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;hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32

.= 0. L by A2, FUNCOP_1:7 ;

:: thesis: verum

for x being Nat holds

( ( x = n implies b