:: 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 Association of Mizar Users
theorem :: ALGSEQ_1:1
canceled;
theorem :: ALGSEQ_1:2
canceled;
theorem :: ALGSEQ_1:3
canceled;
theorem :: ALGSEQ_1:4
canceled;
theorem :: ALGSEQ_1:5
canceled;
theorem :: ALGSEQ_1:6
canceled;
theorem :: ALGSEQ_1:7
canceled;
theorem :: ALGSEQ_1:8
canceled;
theorem :: ALGSEQ_1:9
canceled;
theorem :: ALGSEQ_1:10
theorem :: ALGSEQ_1:11
theorem :: ALGSEQ_1:12
theorem :: ALGSEQ_1:13
theorem :: ALGSEQ_1:14
theorem :: ALGSEQ_1:15
theorem :: ALGSEQ_1:16
theorem :: ALGSEQ_1:17
canceled;
:: deftheorem ALGSEQ_1:def 1 :
canceled;
:: deftheorem Def2 defines finite-Support ALGSEQ_1:def 2 :
:: deftheorem Def3 defines is_at_least_length_of ALGSEQ_1:def 3 :
Lm1:
for R being non empty ZeroStr
for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p
Lm2:
for R being non empty ZeroStr
for p being AlgSequence of R ex k being Element of NAT st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
Lm3:
for k, l being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l
:: deftheorem Def4 defines len ALGSEQ_1:def 4 :
theorem :: ALGSEQ_1:18
canceled;
theorem :: ALGSEQ_1:19
canceled;
theorem :: ALGSEQ_1:20
canceled;
theorem :: ALGSEQ_1:21
canceled;
theorem Th22: :: ALGSEQ_1:22
theorem :: ALGSEQ_1:23
canceled;
theorem Th24: :: ALGSEQ_1:24
theorem Th25: :: ALGSEQ_1:25
:: deftheorem defines support ALGSEQ_1:def 5 :
theorem :: ALGSEQ_1:26
canceled;
theorem :: ALGSEQ_1:27
theorem Th28: :: ALGSEQ_1:28
theorem :: ALGSEQ_1:29
:: deftheorem Def6 defines <% ALGSEQ_1:def 6 :
Lm4:
for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
theorem :: ALGSEQ_1:30
canceled;
theorem Th31: :: ALGSEQ_1:31
theorem :: ALGSEQ_1:32
theorem Th33: :: ALGSEQ_1:33
theorem :: ALGSEQ_1:34