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 . b1 = v . b1 )
assume A6: x in NAT ; :: thesis: u . b1 = v . b1
per cases ( x = n or x <> n ) ;
suppose A7: x = n ; :: thesis: u . b1 = v . b1
hence u . x = a by A4
.= v . x by A5, A7 ;
:: thesis: verum
end;
suppose A8: x <> n ; :: thesis: u . b1 = v . b1
hence u . x = 0. L by A4, A6
.= v . x by A5, A6, A8 ;
:: thesis: verum
end;
end;
end;
hence u = v ; :: thesis: verum