:: Construction of Finite Sequences over Ring and Left-, Right-, :: and Bi-Modules over a Ring :: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba :: :: Received September 13, 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 NUMBERS, NAT_1, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, TARSKI, STRUCT_0, FUNCT_1, SUPINF_2, FUNCOP_1, SUBSET_1, FINSEQ_1, RELAT_1, AFINSQ_1, ALGSEQ_1, POLYNOM1, FINSET_1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, MEMBERED, XCMPLX_0, NAT_1, XXREAL_2, RELAT_1, FUNCT_1, FUNCOP_1, STRUCT_0, FUNCT_2, XXREAL_0, POLYNOM1; constructors FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1, RELSET_1, POLYNOM1, XXREAL_2; registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, FINSET_1, CARD_1, XXREAL_2, MEMBERED; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve i,k,l,m,n for Nat, x for set; :: :: Algebraic Sequences :: reserve R for non empty ZeroStr; definition let R; let F be sequence of R; redefine attr F is finite-Support means :: ALGSEQ_1:def 1 ex n st for i st i >= n holds F.i = 0. R; end; registration let R; cluster finite-Support for sequence of R; end; definition let R; mode AlgSequence of R is finite-Support sequence of R; end; reserve p,q for AlgSequence of R; definition let R,p; let k be Nat; pred k is_at_least_length_of p means :: ALGSEQ_1:def 2 for i st i>=k holds p.i=0.R; end; definition let R,p; func len p -> Element of NAT means :: ALGSEQ_1:def 3 it is_at_least_length_of p & for m st m is_at_least_length_of p holds it<=m; end; ::$CT 7 theorem :: ALGSEQ_1:8 i>=len p implies p.i=0.R; theorem :: ALGSEQ_1:9 (for i st i < k holds p.i<>0.R) implies len p>=k; theorem :: ALGSEQ_1:10 len p=k+1 implies p.k<>0.R; scheme :: ALGSEQ_1:sch 1 AlgSeqLambdaF{R()->non empty ZeroStr,A()->Nat, F(Nat)->Element of R()}: ex p being AlgSequence of R() st len p <= A() & for k st k < A() holds p.k=F(k); ::$CT theorem :: ALGSEQ_1:12 len p = len q & (for k st k < len p holds p.k = q.k) implies p=q; theorem :: ALGSEQ_1:13 the carrier of R <> {0.R} implies for k ex p being AlgSequence of R st len p = k; :: :: The Short AlgSequence of R :: reserve x for Element of R; definition ::$CD let R,x; func <%x%> -> AlgSequence of R means :: ALGSEQ_1:def 5 len it <= 1 & it.0 = x; end; theorem :: ALGSEQ_1:14 p=<%0.R%> iff len p = 0; ::$CT theorem :: ALGSEQ_1:16 <%0.R%>.i=0.R; theorem :: ALGSEQ_1:17 p=<%0.R%> iff rng p = {0.R};