begin
theorem Th1:
theorem
theorem Th3:
:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :
theorem Th4:
theorem Th5:
theorem Th6:
definition
let L be non
empty 1-sorted ;
let N be non
empty NetStr of
L;
let f be
Function of
N,
N;
func N * f -> non
empty strict NetStr of
L means :
Def2:
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) & the
mapping of
it = the
mapping of
N * f );
existence
ex b1 being non empty strict NetStr of L st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = the mapping of N * f )
uniqueness
for b1, b2 being non empty strict NetStr of L st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = the mapping of N * f & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b2 = the mapping of N * f holds
b1 = b2
;
end;
:: deftheorem Def2 defines * WAYBEL28:def 2 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem
theorem Th15:
:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def 3 :
theorem
theorem Th17:
:: deftheorem defines xi WAYBEL28:def 4 :
theorem
theorem
theorem
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem