let u, v be Polynomial of L; ( ( 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 ) )
; u = v
hence
u = v
; verum