begin
:: deftheorem Def1 defines union TMAP_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem
theorem
for
A,
B being non
empty set for
A1,
A2,
A3,
A12,
A23 being non
empty Subset of st
A12 = A1 \/ A2 &
A23 = A2 \/ A3 holds
for
f1 being
Function of
A1,
B for
f2 being
Function of
A2,
B for
f3 being
Function of
A3,
B st
f1 | (A1 /\ A2) = f2 | (A1 /\ A2) &
f2 | (A2 /\ A3) = f3 | (A2 /\ A3) &
f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds
for
f12 being
Function of
A12,
B for
f23 being
Function of
A23,
B st
f12 = f1 union f2 &
f23 = f2 union f3 holds
f12 union f3 = f1 union f23
theorem
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem Th46:
begin
:: deftheorem Def2 defines is_continuous_at TMAP_1:def 2 :
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem Th56:
theorem
:: deftheorem defines | TMAP_1:def 3 :
theorem
canceled;
theorem Th59:
theorem Th60:
theorem
theorem
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem
:: deftheorem Def4 defines | TMAP_1:def 4 :
theorem Th72:
theorem
theorem Th74:
theorem Th75:
theorem
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem
theorem Th86:
theorem
theorem Th88:
theorem Th89:
theorem Th90:
theorem
theorem
theorem
theorem Th94:
:: deftheorem TMAP_1:def 5 :
canceled;
:: deftheorem defines incl TMAP_1:def 6 :
theorem
theorem
theorem
theorem
begin
:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 7 :
theorem Th99:
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
:: deftheorem defines modified_with_respect_to TMAP_1:def 8 :
theorem
theorem Th105:
theorem Th106:
:: deftheorem defines modid TMAP_1:def 9 :
theorem
canceled;
theorem Th108:
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
:: deftheorem Def10 defines modified_with_respect_to TMAP_1:def 10 :
theorem Th114:
theorem
theorem
:: deftheorem Def11 defines modid TMAP_1:def 11 :
theorem
theorem Th118:
theorem Th119:
theorem
theorem
theorem
begin
theorem Th123:
theorem
theorem
theorem Th126:
theorem Th127:
theorem Th128:
theorem Th129:
theorem
theorem
theorem Th132:
theorem Th133:
theorem Th134:
theorem Th135:
theorem Th136:
theorem
begin
:: deftheorem Def12 defines union TMAP_1:def 12 :
theorem Th138:
theorem
theorem Th140:
theorem
theorem
theorem
theorem
theorem Th145:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem