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
A6: dom u = NAT by FUNCT_2:def 1;
A7: dom v = NAT by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in NAT implies u . b₁ = v . b₁ )
assume x in NAT ; :: thesis: u . b₁ = v . b₁
then A8: x is Nat ;

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

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

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

end;

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

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

end;

end;

end;

hence u = v by A6, A7, FUNCT_1:9; :: thesis: verum