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: now

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

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

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

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

end;

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

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

end;

end;

end;

( dom u = NAT & dom v = NAT ) by FUNCT_2:def 1;
hence u = v by A6, FUNCT_1:2; :: thesis: verum