:: The Tichonov Theorem
:: by Bart{\l}omiej Skorulski
::
:: Received May 23, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: YELLOW17:1
theorem Th2: :: YELLOW17:2
theorem Th3: :: YELLOW17:3
theorem Th4: :: YELLOW17:4
theorem Th5: :: YELLOW17:5
Lm1:
for F, g being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st i1 <> i2 & g in product F & g +* i1,xi1 in (proj F,i2) " Ai2 holds
g in (proj F,i2) " Ai2
theorem Th6: :: YELLOW17:6
theorem Th7: :: YELLOW17:7
theorem Th8: :: YELLOW17:8
theorem Th9: :: YELLOW17:9
theorem Th10: :: YELLOW17:10
theorem Th11: :: YELLOW17:11
theorem Th12: :: YELLOW17:12
theorem Th13: :: YELLOW17:13
theorem :: YELLOW17:14
canceled;
theorem Th15: :: YELLOW17:15
theorem Th16: :: YELLOW17:16
theorem Th17: :: YELLOW17:17
theorem Th18: :: YELLOW17:18
theorem Th19: :: YELLOW17:19
theorem Th20: :: YELLOW17:20
theorem Th21: :: YELLOW17:21
theorem Th22: :: YELLOW17:22
theorem Th23: :: YELLOW17:23
theorem :: YELLOW17:24