begin
theorem
canceled;
theorem
canceled;
theorem
theorem Th4:
theorem Th5:
theorem
theorem Th7:
:: deftheorem AFINSQ_1:def 1 :
canceled;
theorem
scheme
XSeqEx{
F1()
-> Nat,
P1[
set ,
set ] } :
provided
A1:
for
k being
Nat st
k in F1() holds
ex
x being
set st
P1[
k,
x]
theorem
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
theorem Th13:
theorem Th15:
theorem Th3:
theorem Th17:
theorem X:
theorem Th19:
:: deftheorem defines <% AFINSQ_1:def 2 :
:: deftheorem defines <%> AFINSQ_1:def 3 :
:: deftheorem Def4 defines ^ AFINSQ_1:def 4 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
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
:: 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
theorem Th36:
theorem
canceled;
theorem
theorem Th39:
theorem Th40:
theorem
theorem Th42:
theorem Th43:
theorem Tex:
theorem
:: deftheorem Def8 defines ^omega AFINSQ_1:def 8 :
theorem
theorem
theorem
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem
theorem
theorem
theorem Th111:
theorem Th121:
theorem
theorem TTT:
theorem Th1:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def1 defines FS2XFS AFINSQ_1:def 9 :
:: deftheorem defines XFS2FS AFINSQ_1:def 10 :
theorem Th4:
:: deftheorem Def3 defines FS2XFS* AFINSQ_1:def 11 :
:: deftheorem Def4 defines XFS2FS* AFINSQ_1:def 12 :
theorem Th5: