let u, v be Polynomial of L; :: thesis: ( ( for x being Nat holds
( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) ) & ( for x being Nat holds
( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ) implies u = v )
assume that
A4: for x being Nat holds
( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) and
A5: for x being Nat holds
( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ; :: thesis: u = v

now :: thesis: for x being object st x in NAT holds
u . x = v . x

let x be object ; :: thesis: ( x in NAT implies u . b₁ = v . b₁ )
assume A6: x in NAT ; :: thesis: u . b₁ = v . b₁

per cases ( x = n or x <> n ) ;

suppose A7: x = n ; :: thesis: u . b₁ = v . b₁

hence u . x = a by A4
.= v . x by A5, A7 ;
:: thesis: verum

end;

suppose A8: x <> n ; :: thesis: u . b₁ = v . b₁

hence u . x = 0. L by A4, A6
.= v . x by A5, A6, A8 ;
:: thesis: verum

end;

end;

end;

hence u = v ; :: thesis: verum