begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem
theorem Th7:
:: deftheorem AFINSQ_1:def 1 :
canceled;
theorem
theorem
theorem Th10:
theorem
theorem Th12:
theorem
theorem
theorem Th15:
theorem
theorem
theorem
theorem Th19:
:: deftheorem defines <% AFINSQ_1:def 2 :
:: deftheorem defines <%> AFINSQ_1:def 3 :
:: deftheorem Def4 defines ^ AFINSQ_1:def 4 :
theorem
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem
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
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