:: Solution of Cubic and Quartic Equations
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users
begin
theorem
Th1
:
:: POLYEQ_5:1
for
a
being
complex
number
holds
a
*
a
=
a
|^
2
proof
end;