:: Zero Based Finite Sequences
:: by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received September 28, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: AFINSQ_1:1
theorem Th2: :: AFINSQ_1:2
theorem :: AFINSQ_1:3
theorem Th4: :: AFINSQ_1:4
theorem Th5: :: AFINSQ_1:5
theorem :: AFINSQ_1:6
theorem Th7: :: AFINSQ_1:7
:: deftheorem AFINSQ_1:def 1 :
canceled;
theorem :: AFINSQ_1:8
theorem :: AFINSQ_1:9
theorem Th10: :: AFINSQ_1:10
theorem :: AFINSQ_1:11
theorem Th12: :: AFINSQ_1:12
theorem :: AFINSQ_1:13
theorem :: AFINSQ_1:14
theorem Th15: :: AFINSQ_1:15
theorem :: AFINSQ_1:16
theorem :: AFINSQ_1:17
theorem :: AFINSQ_1:18
theorem Th19: :: AFINSQ_1:19
:: deftheorem defines <% AFINSQ_1:def 2 :
:: deftheorem defines <%> AFINSQ_1:def 3 :
:: deftheorem Def4 defines ^ AFINSQ_1:def 4 :
theorem :: AFINSQ_1:20
theorem Th21: :: AFINSQ_1:21
theorem :: AFINSQ_1:22
theorem Th23: :: AFINSQ_1:23
theorem Th24: :: AFINSQ_1:24
theorem Th25: :: AFINSQ_1:25
theorem Th26: :: AFINSQ_1:26
theorem Th27: :: AFINSQ_1:27
theorem Th28: :: AFINSQ_1:28
theorem Th29: :: AFINSQ_1:29
theorem Th30: :: AFINSQ_1:30
theorem :: AFINSQ_1:31
theorem Th32: :: AFINSQ_1:32
theorem :: AFINSQ_1:33
Lm1:
for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
:: deftheorem Def5 defines <% AFINSQ_1:def 5 :
theorem :: AFINSQ_1:34
:: deftheorem defines <% AFINSQ_1:def 6 :
:: deftheorem defines <% AFINSQ_1:def 7 :
registration
let x,
y be
set ;
cluster <%x,y%> -> Relation-like Function-like ;
coherence
( <%x,y%> is Function-like & <%x,y%> is Relation-like )
;
let z be
set ;
cluster <%x,y,z%> -> Relation-like Function-like ;
coherence
( <%x,y,z%> is Function-like & <%x,y,z%> is Relation-like )
;
end;
registration
let x,
y be
set ;
cluster <%x,y%> -> T-Sequence-like finite ;
coherence
( <%x,y%> is finite & <%x,y%> is T-Sequence-like )
;
let z be
set ;
cluster <%x,y,z%> -> T-Sequence-like finite ;
coherence
( <%x,y,z%> is finite & <%x,y,z%> is T-Sequence-like )
;
end;
theorem :: AFINSQ_1:35
theorem Th36: :: AFINSQ_1:36
theorem :: AFINSQ_1:37
canceled;
theorem :: AFINSQ_1:38
theorem :: AFINSQ_1:39
theorem :: AFINSQ_1:40
theorem :: AFINSQ_1:41
theorem Th42: :: AFINSQ_1:42
theorem :: AFINSQ_1:43
theorem Tex: :: AFINSQ_1:44
theorem :: AFINSQ_1:45
:: deftheorem Def8 defines ^omega AFINSQ_1:def 8 :
theorem :: AFINSQ_1:46
theorem :: AFINSQ_1:47
theorem :: AFINSQ_1:48