begin
Lm1:
for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D
;
Lm2:
for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D
;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
Lm3:
for D being non empty set
for f being FinSequence of D holds Rev f is FinSequence of D
;
:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :
begin
:: deftheorem Def2 defines full BINTREE2:def 2 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines FinSeqLevel BINTREE2:def 3 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem
theorem