:: Ordered Rings - Part I :: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba :: :: Received October 11, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NAT_1, XBOOLE_0, ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4, RELAT_1, ARYTM_3, PARTFUN1, XXREAL_0, CARD_1, FUNCT_1, SQUARE_1, O_RING_1; notations ORDINAL1, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, XXREAL_0; constructors RLVECT_1, PARTFUN1, XXREAL_0, NAT_1, VECTSP_1, RELSET_1, GROUP_1; registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, NAT_1; requirements NUMERALS, SUBSET, ARITHM; begin :: Field-like Algebras reserve i,j,k,m,n for Nat; reserve R for non empty doubleLoopStr; reserve x,y for Scalar of R; reserve f,g,h for FinSequence of R; definition let R be non empty doubleLoopStr, x be Scalar of R; func x^2 -> Scalar of R equals :: O_RING_1:def 1 x*x; end; definition let R be non empty doubleLoopStr, x be Scalar of R; attr x is being_a_square means :: O_RING_1:def 2 ex y being Scalar of R st x=y^2; end; definition let R,f; attr f is being_a_Sum_of_squares means :: O_RING_1:def 3 len f<>0 & f/.1 is being_a_square & for n st n<>0 & n0 & f/.1 is being_a_square & for n st n<>0 & n0 & f/.1 is being_a_product_of_squares & for n st n<>0 & n0 & for n st n<>0 & n<=len f holds f/.n is being_a_product_of_squares or ex i,j st f/.n=f/.i*f/.j & i<>0 & i0 & j0 & f/.1 is being_an_amalgam_of_squares & for n st n<>0 & n0 & for n st n<>0 & n<=len f holds f/.n is being_an_amalgam_of_squares or ex i,j st (f/.n=f /.i*f/.j or f/.n=f/.i+f/.j) & i<>0 & i0 & j