:: YELLOW17 semantic presentation

begin

theorem Th1: :: YELLOW17:1
for F being Function
for i, xi being set
for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
proof
let F be Function; ::_thesis: for i, xi being set
for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
let i, xi be set ; ::_thesis: for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
let Ai be Subset of (F . i); ::_thesis: ( (proj (F,i)) " {xi} meets (proj (F,i)) " Ai implies xi in Ai )
set f = the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai);
assume A1: ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: xi in Ai
then  the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in (proj (F,i)) " {xi} by XBOOLE_0:def_4;
then  (proj (F,i)) . the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in {xi} by FUNCT_1:def_7;
then A2: (proj (F,i)) . the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) = xi by TARSKI:def_1;
 the Element of ((proj (F,i)) " {xi}) /\ ((proj (F,i)) " Ai) in (proj (F,i)) " Ai by A1, XBOOLE_0:def_4;
hence  xi in Ai by A2, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th2: :: YELLOW17:2
for F, f being Function
for i, xi being set st xi in F . i & f in product F holds
f +* (i,xi) in product F
proof
let F, f be Function; ::_thesis: for i, xi being set st xi in F . i & f in product F holds
f +* (i,xi) in product F
let i, xi be set ; ::_thesis: ( xi in F . i & f in product F implies f +* (i,xi) in product F )
assume A1: xi in F . i ; ::_thesis: ( not f in product F or f +* (i,xi) in product F )
assume A2: f in product F ; ::_thesis: f +* (i,xi) in product F
A3: for x being set st x in dom F holds
(f +* (i,xi)) . x in F . x
proof
let x be set ; ::_thesis: ( x in dom F implies (f +* (i,xi)) . x in F . x )
assume A4: x in dom F ; ::_thesis: (f +* (i,xi)) . x in F . x
percases ( i = x or i <> x ) ;
supposeA5: i = x ; ::_thesis: (f +* (i,xi)) . x in F . x
thus  (f +* (i,xi)) . x in F . x ::_thesis: verum
proof
percases ( i in dom f or not i in dom f ) ;
suppose i in dom f ; ::_thesis: (f +* (i,xi)) . x in F . x
hence  (f +* (i,xi)) . x in F . x by A1, A5, FUNCT_7:31; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (f +* (i,xi)) . x in F . x
then  f +* (i,xi) = f by FUNCT_7:def_3;
hence  (f +* (i,xi)) . x in F . x by A2, A4, CARD_3:9; ::_thesis: verum
end;
end;
end;
end;
suppose i <> x ; ::_thesis: (f +* (i,xi)) . x in F . x
then  (f +* (i,xi)) . x = f . x by FUNCT_7:32;
hence  (f +* (i,xi)) . x in F . x by A2, A4, CARD_3:9; ::_thesis: verum
end;
end;
end;
 dom f = dom F by A2, CARD_3:9;
then  dom (f +* (i,xi)) = dom F by FUNCT_7:30;
hence  f +* (i,xi) in product F by A3, CARD_3:9; ::_thesis: verum
end;

theorem Th3: :: YELLOW17:3
for F being Function
for i being set st i in dom F holds
( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
proof
let F be Function; ::_thesis: for i being set st i in dom F holds
( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
let i be set ; ::_thesis: ( i in dom F implies ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) ) )
assume A1: i in dom F ; ::_thesis: ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
thus A0: rng (proj (F,i)) c= F . i ::_thesis: ( product F <> {} implies rng (proj (F,i)) = F . i )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (proj (F,i)) or x in F . i )
assume  x in rng (proj (F,i)) ; ::_thesis: x in F . i
then consider f9 being set  such that
A3: f9 in dom (proj (F,i)) and
A4: x = (proj (F,i)) . f9 by FUNCT_1:def_3;
 f9 in product F by A3;
then consider f being Function such that
A5: f9 = f and
 dom f = dom F and
A6: for x being set st x in dom F holds
f . x in F . x by CARD_3:def_5;
 (proj (F,i)) . f = f . i by A3, A5, CARD_3:def_16;
hence  x in F . i by A1, A4, A5, A6; ::_thesis: verum
end;
assume A2: product F <> {} ; ::_thesis: rng (proj (F,i)) = F . i
thus  rng (proj (F,i)) c= F . i by A0; :: according to XBOOLE_0:def_10 ::_thesis: F . i c= rng (proj (F,i))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F . i or x in rng (proj (F,i)) )
set f9 = the Element of product F;
consider f being Function such that
A7: the Element of product F = f and
A8: dom f = dom F and
 for x being set st x in dom F holds
f . x in F . x by A2, CARD_3:def_5;
assume  x in F . i ; ::_thesis: x in rng (proj (F,i))
then  f +* (i,x) in product F by A2, A7, Th2;
then A9: f +* (i,x) in dom (proj (F,i)) by CARD_3:def_16;
 (f +* (i,x)) . i = x by A1, A8, FUNCT_7:31;
then  (proj (F,i)) . (f +* (i,x)) = x by A9, CARD_3:def_16;
hence  x in rng (proj (F,i)) by A9, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th4: :: YELLOW17:4
for F being Function
for i being set st i in dom F holds
(proj (F,i)) " (F . i) = product F
proof
let F be Function; ::_thesis: for i being set st i in dom F holds
(proj (F,i)) " (F . i) = product F
let i be set ; ::_thesis: ( i in dom F implies (proj (F,i)) " (F . i) = product F )
assume A1: i in dom F ; ::_thesis: (proj (F,i)) " (F . i) = product F
 dom (proj (F,i)) = product F by CARD_3:def_16;
hence  (proj (F,i)) " (F . i) c= product F by RELAT_1:132; :: according to XBOOLE_0:def_10 ::_thesis: product F c= (proj (F,i)) " (F . i)
let f9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not f9 in product F or f9 in (proj (F,i)) " (F . i) )
assume A2: f9 in product F ; ::_thesis: f9 in (proj (F,i)) " (F . i)
then consider f being Function such that
A3: f9 = f and
 dom f = dom F and
A4: for x being set st x in dom F holds
f . x in F . x by CARD_3:def_5;
A5: f in dom (proj (F,i)) by A2, A3, CARD_3:def_16;
 f . i in F . i by A1, A4;
then  (proj (F,i)) . f in F . i by A5, CARD_3:def_16;
hence  f9 in (proj (F,i)) " (F . i) by A3, A5, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th5: :: YELLOW17:5
for F, f being Function
for i, xi being set st xi in F . i & i in dom F & f in product F holds
f +* (i,xi) in (proj (F,i)) " {xi}
proof
let F, f be Function; ::_thesis: for i, xi being set st xi in F . i & i in dom F & f in product F holds
f +* (i,xi) in (proj (F,i)) " {xi}
let i, xi be set ; ::_thesis: ( xi in F . i & i in dom F & f in product F implies f +* (i,xi) in (proj (F,i)) " {xi} )
assume that
A1: xi in F . i and
A2: i in dom F and
A3: f in product F ; ::_thesis: f +* (i,xi) in (proj (F,i)) " {xi}
 f +* (i,xi) in product F by A1, A3, Th2;
then A4: f +* (i,xi) in dom (proj (F,i)) by CARD_3:def_16;
 i in dom f by A2, A3, CARD_3:9;
then  (f +* (i,xi)) . i = xi by FUNCT_7:31;
then  (f +* (i,xi)) . i in {xi} by TARSKI:def_1;
then  (proj (F,i)) . (f +* (i,xi)) in {xi} by A4, CARD_3:def_16;
hence  f +* (i,xi) in (proj (F,i)) " {xi} by A4, FUNCT_1:def_7; ::_thesis: verum
end;

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
proof
let F, g be Function; ::_thesis: 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
let i1, i2, xi1 be set ; ::_thesis: 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
let Ai2 be Subset of (F . i2); ::_thesis: ( i1 <> i2 & g in product F & g +* (i1,xi1) in (proj (F,i2)) " Ai2 implies g in (proj (F,i2)) " Ai2 )
assume that
A1: i1 <> i2 and
A2: g in product F ; ::_thesis: ( not g +* (i1,xi1) in (proj (F,i2)) " Ai2 or g in (proj (F,i2)) " Ai2 )
A3: g in dom (proj (F,i2)) by A2, CARD_3:def_16;
assume  g +* (i1,xi1) in (proj (F,i2)) " Ai2 ; ::_thesis: g in (proj (F,i2)) " Ai2
then  ( g +* (i1,xi1) in dom (proj (F,i2)) & (proj (F,i2)) . (g +* (i1,xi1)) in Ai2 ) by FUNCT_1:def_7;
then  (g +* (i1,xi1)) . i2 in Ai2 by CARD_3:def_16;
then  g . i2 in Ai2 by A1, FUNCT_7:32;
then  (proj (F,i2)) . g in Ai2 by A3, CARD_3:def_16;
hence  g in (proj (F,i2)) " Ai2 by A3, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th6: :: YELLOW17:6
for F, f being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds
( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
proof
let F, f be Function; ::_thesis: for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds
( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
let i1, i2, xi1 be set ; ::_thesis: for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds
( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
let Ai2 be Subset of (F . i2); ::_thesis: ( xi1 in F . i1 & f in product F & i1 <> i2 implies ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) )
assume that
A1: xi1 in F . i1 and
A2: f in product F ; ::_thesis: ( not i1 <> i2 or ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) )
assume A3: i1 <> i2 ; ::_thesis: ( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
thus  ( f in (proj (F,i2)) " Ai2 implies f +* (i1,xi1) in (proj (F,i2)) " Ai2 ) ::_thesis: ( f +* (i1,xi1) in (proj (F,i2)) " Ai2 implies f in (proj (F,i2)) " Ai2 )
proof
A4: (f +* (i1,xi1)) +* (i1,(f . i1)) = f +* (i1,(f . i1)) by FUNCT_7:34
.= f by FUNCT_7:35 ;
assume  f in (proj (F,i2)) " Ai2 ; ::_thesis: f +* (i1,xi1) in (proj (F,i2)) " Ai2
hence  f +* (i1,xi1) in (proj (F,i2)) " Ai2 by A1, A2, A3, A4, Lm1, Th2; ::_thesis: verum
end;
assume  f +* (i1,xi1) in (proj (F,i2)) " Ai2 ; ::_thesis: f in (proj (F,i2)) " Ai2
hence  f in (proj (F,i2)) " Ai2 by A2, A3, Lm1; ::_thesis: verum
end;

theorem Th7: :: YELLOW17:7
for F being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds
( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
proof
let F be Function; ::_thesis: for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds
( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let i1, i2, xi1 be set ; ::_thesis: for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds
( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let Ai2 be Subset of (F . i2); ::_thesis: ( product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 implies ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) )
assume that
A1: product F <> {} and
A2: xi1 in F . i1 and
A3: i1 in dom F and
A4: i2 in dom F and
A5: Ai2 <> F . i2 ; ::_thesis: ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
set f9 = the Element of product F;
consider f being Function such that
A6: the Element of product F = f and
A7: dom f = dom F and
 for x being set st x in dom F holds
f . x in F . x by A1, CARD_3:def_5;
 not F . i2 c= Ai2 by A5, XBOOLE_0:def_10;
then consider xi2 being set  such that
A8: xi2 in F . i2 and
A9: not xi2 in Ai2 by TARSKI:def_3;
reconsider xi2 = xi2 as Element of F . i2 by A8;
A10: (f +* (i2,xi2)) . i2 = xi2 by A4, A7, FUNCT_7:31;
thus  ( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 implies ( i1 = i2 & xi1 in Ai2 ) ) ::_thesis: ( i1 = i2 & xi1 in Ai2 implies (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 )
proof
assume A11: (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 ; ::_thesis: ( i1 = i2 & xi1 in Ai2 )
thus A12: i1 = i2 ::_thesis: xi1 in Ai2
proof
assume A13: i1 <> i2 ; ::_thesis: contradiction
 ( f +* (i2,xi2) in product F & (f +* (i2,xi2)) +* (i1,xi1) in (proj (F,i1)) " {xi1} ) by A1, A2, A3, A8, A6, Th2, Th5;
then  f +* (i2,xi2) in (proj (F,i2)) " Ai2 by A2, A11, A13, Th6;
then  ( f +* (i2,xi2) in dom (proj (F,i2)) & (proj (F,i2)) . (f +* (i2,xi2)) in Ai2 ) by FUNCT_1:def_7;
hence  contradiction by A9, A10, CARD_3:def_16; ::_thesis: verum
end;
 xi1 in rng (proj (F,i1)) by A1, A2, A3, Th3;
then  {xi1} c= rng (proj (F,i1)) by ZFMISC_1:31;
then  {xi1} c= Ai2 by A11, A12, FUNCT_1:88;
hence  xi1 in Ai2 by ZFMISC_1:31; ::_thesis: verum
end;
assume that
A14: i1 = i2 and
A15: xi1 in Ai2 ; ::_thesis: (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2
 {xi1} c= Ai2 by A15, ZFMISC_1:31;
hence  (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 by A14, RELAT_1:143; ::_thesis: verum
end;

scheme :: YELLOW17:sch 1
ElProductEx{ F1() ->  non empty set , F2() ->  non-Empty TopStruct-yielding ManySortedSet of F1(), P1[ set , set ] } :
 ex f being Element of (product F2()) st
for i being Element of F1() holds P1[f . i,i]
provided
A1: for i being Element of F1() ex x being Element of (F2() . i) st P1[x,i]
proof
defpred S1[ set , set ] means ( P1[$2,$1] & ( for i9 being Element of F1() st $1 = i9 holds
$2 in the carrier of (F2() . i9) ) );
A2: for i being set st i in F1() holds
ex x being set st S1[i,x]
proof
let i be set ; ::_thesis: ( i in F1() implies ex x being set st S1[i,x] )
assume  i in F1() ; ::_thesis: ex x being set st S1[i,x]
then reconsider i1 = i as Element of F1() ;
consider x being Element of (F2() . i1) such that
A3: P1[x,i1] by A1;
take  x ; ::_thesis: S1[i,x]
thus  P1[x,i] by A3; ::_thesis: for i9 being Element of F1() st i = i9 holds
x in the carrier of (F2() . i9)
let i9 be Element of F1(); ::_thesis: ( i = i9 implies x in the carrier of (F2() . i9) )
assume  i = i9 ; ::_thesis: x in the carrier of (F2() . i9)
hence  x in the carrier of (F2() . i9) ; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = F1() and
A5: for i being set st i in F1() holds
S1[i,f . i] from CLASSES1:sch_1(A2);
A6: for x being set st x in dom (Carrier F2()) holds
f . x in (Carrier F2()) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier F2()) implies f . x in (Carrier F2()) . x )
assume  x in dom (Carrier F2()) ; ::_thesis: f . x in (Carrier F2()) . x
then reconsider x9 = x as Element of F1() ;
 f . x9 in the carrier of (F2() . x9) by A5;
hence  f . x in (Carrier F2()) . x by YELLOW_6:2; ::_thesis: verum
end;
 dom f = dom (Carrier F2()) by A4, PARTFUN1:def_2;
then  f in product (Carrier F2()) by A6, CARD_3:9;
then reconsider f = f as Element of (product F2()) by WAYBEL18:def_3;
take  f ; ::_thesis: for i being Element of F1() holds P1[f . i,i]
let i be Element of F1(); ::_thesis: P1[f . i,i]
thus  P1[f . i,i] by A5; ::_thesis: verum
end;

theorem Th8: :: YELLOW17:8
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
let i be Element of I; ::_thesis: for f being Element of (product J) holds (proj (J,i)) . f = f . i
let f be Element of (product J); ::_thesis: (proj (J,i)) . f = f . i
 f in the carrier of (product J) ;
then  f in product (Carrier J) by WAYBEL18:def_3;
then  f in dom (proj ((Carrier J),i)) by CARD_3:def_16;
then  (proj ((Carrier J),i)) . f = f . i by CARD_3:def_16;
hence  (proj (J,i)) . f = f . i by WAYBEL18:def_4; ::_thesis: verum
end;

theorem Th9: :: YELLOW17:9
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
let i be Element of I; ::_thesis: for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
let xi be Element of (J . i); ::_thesis: for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
let Ai be Subset of (J . i); ::_thesis: ( (proj (J,i)) " {xi} meets (proj (J,i)) " Ai implies xi in Ai )
assume  ((proj (J,i)) " {xi}) /\ ((proj (J,i)) " Ai) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: xi in Ai
then  ((proj ((Carrier J),i)) " {xi}) /\ ((proj (J,i)) " Ai) <> {} by WAYBEL18:def_4;
then  ((proj ((Carrier J),i)) " {xi}) /\ ((proj ((Carrier J),i)) " Ai) <> {} by WAYBEL18:def_4;
then A1: (proj ((Carrier J),i)) " {xi} meets (proj ((Carrier J),i)) " Ai by XBOOLE_0:def_7;
 Ai c= the carrier of (J . i) ;
then  Ai c= (Carrier J) . i by YELLOW_6:2;
hence  xi in Ai by A1, Th1; ::_thesis: verum
end;

theorem Th10: :: YELLOW17:10
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)
let i be Element of I; ::_thesis: (proj (J,i)) " ([#] (J . i)) = [#] (product J)
 i in I ;
then  i in dom (Carrier J) by PARTFUN1:def_2;
then  (proj ((Carrier J),i)) " ((Carrier J) . i) = product (Carrier J) by Th4;
then  (proj ((Carrier J),i)) " ((Carrier J) . i) = [#] (product J) by WAYBEL18:def_3;
then  (proj ((Carrier J),i)) " ([#] (J . i)) = [#] (product J) by YELLOW_6:2;
hence  (proj (J,i)) " ([#] (J . i)) = [#] (product J) by WAYBEL18:def_4; ::_thesis: verum
end;

theorem Th11: :: YELLOW17:11
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
let i be Element of I; ::_thesis: for xi being Element of (J . i)
for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
let xi be Element of (J . i); ::_thesis: for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
let f be Element of (product J); ::_thesis: f +* (i,xi) in (proj (J,i)) " {xi}
 xi in the carrier of (J . i) ;
then A1: xi in (Carrier J) . i by YELLOW_6:2;
 f in the carrier of (product J) ;
then A2: f in product (Carrier J) by WAYBEL18:def_3;
 i in I ;
then  i in dom (Carrier J) by PARTFUN1:def_2;
then  f +* (i,xi) in (proj ((Carrier J),i)) " {xi} by A1, A2, Th5;
hence  f +* (i,xi) in (proj (J,i)) " {xi} by WAYBEL18:def_4; ::_thesis: verum
end;

theorem Th12: :: YELLOW17:12
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let i1, i2 be Element of I; ::_thesis: for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let xi1 be Element of (J . i1); ::_thesis: for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let Ai2 be Subset of (J . i2); ::_thesis: ( Ai2 <> [#] (J . i2) implies ( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) )
reconsider Ai29 = Ai2 as Subset of ((Carrier J) . i2) by YELLOW_6:2;
 i2 in I ;
then A1: i2 in dom (Carrier J) by PARTFUN1:def_2;
assume  Ai2 <> [#] (J . i2) ; ::_thesis: ( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
then A2: Ai29 <> (Carrier J) . i2 by YELLOW_6:2;
 xi1 in the carrier of (J . i1) ;
then A3: xi1 in (Carrier J) . i1 by YELLOW_6:2;
 i1 in I ;
then  ( product (Carrier J) <> {} & i1 in dom (Carrier J) ) by PARTFUN1:def_2;
then  ( (proj ((Carrier J),i1)) " {xi1} c= (proj ((Carrier J),i2)) " Ai29 iff ( i1 = i2 & xi1 in Ai29 ) ) by A1, A3, A2, Th7;
then  ( (proj (J,i1)) " {xi1} c= (proj ((Carrier J),i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai29 ) ) by WAYBEL18:def_4;
hence  ( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) by WAYBEL18:def_4; ::_thesis: verum
end;

theorem Th13: :: YELLOW17:13
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
let i1, i2 be Element of I; ::_thesis: for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
let xi1 be Element of (J . i1); ::_thesis: for Ai2 being Subset of (J . i2)
for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
let Ai2 be Subset of (J . i2); ::_thesis: for f being Element of (product J) st i1 <> i2 holds
( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
let f be Element of (product J); ::_thesis: ( i1 <> i2 implies ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) )
reconsider Ai29 = Ai2 as Subset of ((Carrier J) . i2) by YELLOW_6:2;
 xi1 in the carrier of (J . i1) ;
then A1: xi1 in (Carrier J) . i1 by YELLOW_6:2;
 f in the carrier of (product J) ;
then A2: f in product (Carrier J) by WAYBEL18:def_3;
assume  i1 <> i2 ; ::_thesis: ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )
then  ( f in (proj ((Carrier J),i2)) " Ai29 iff f +* (i1,xi1) in (proj ((Carrier J),i2)) " Ai29 ) by A1, A2, Th6;
hence  ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) by WAYBEL18:def_4; ::_thesis: verum
end;

begin

theorem Th14: :: YELLOW17:14
for T being non empty TopStruct holds
( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )
proof
let T be non empty TopStruct ; ::_thesis: ( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )
thus  ( T is compact implies for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) ) ::_thesis: ( ( for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) ) implies T is compact )
proof
assume A1: T is compact ; ::_thesis: for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite )
let F be Subset-Family of T; ::_thesis: ( F is open & [#] T c= union F implies ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )
assume that
A2: F is open and
A3: [#] T c= union F ; ::_thesis: ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite )
 F is Cover of T by A3, TOPMETR:1;
then consider G being Subset-Family of T such that
A4: ( G c= F & G is Cover of T & G is finite ) by A1, A2, COMPTS_1:def_1;
take  G ; ::_thesis: ( G c= F & [#] T c= union G & G is finite )
thus  ( G c= F & [#] T c= union G & G is finite ) by A4, TOPMETR:1; ::_thesis: verum
end;
assume A5: for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) ; ::_thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( not F is M4( the carrier of T) or not F is open or ex b1 being Element of bool (bool the carrier of T) st
( b1 c= F & b1 is M4( the carrier of T) & b1 is finite ) )
assume that
A6: F is Cover of T and
A7: F is open ; ::_thesis: ex b1 being Element of bool (bool the carrier of T) st
( b1 c= F & b1 is M4( the carrier of T) & b1 is finite )
 [#] T c= union F by A6, TOPMETR:1;
then consider G being Subset-Family of T such that
A8: ( G c= F & [#] T c= union G & G is finite ) by A5, A7;
take  G ; ::_thesis: ( G c= F & G is M4( the carrier of T) & G is finite )
thus  ( G c= F & G is M4( the carrier of T) & G is finite ) by A8, TOPMETR:1; ::_thesis: verum
end;

theorem Th15: :: YELLOW17:15
for T being non empty TopSpace
for B being prebasis of T holds
( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )
proof
let T be non empty TopSpace; ::_thesis: for B being prebasis of T holds
( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )
let B be prebasis of T; ::_thesis: ( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )
set x = the carrier of T;
 the carrier of T in the topology of T by PRE_TOPC:def_1;
then reconsider x = the carrier of T as Element of (InclPoset the topology of T) by YELLOW_1:1;
 ( x is compact iff x << x ) by WAYBEL_3:def_2;
hence  ( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G ) by WAYBEL_3:37, WAYBEL_7:31; ::_thesis: verum
end;

begin

theorem Th16: :: YELLOW17:16
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
let A be set ; ::_thesis: ( A in product_prebasis J implies ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A ) )
assume  A in product_prebasis J ; ::_thesis: ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
then consider i being set , T being TopStruct , Ai being Subset of T such that
A1: i in I and
A2: Ai is open and
A3: T = J . i and
A4: A = product ((Carrier J) +* (i,Ai)) by WAYBEL18:def_2;
reconsider i = i as Element of I by A1;
reconsider Ai = Ai as Subset of (J . i) by A3;
take  i ; ::_thesis: ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
take  Ai ; ::_thesis: ( Ai is open & (proj (J,i)) " Ai = A )
thus  Ai is open by A2, A3; ::_thesis: (proj (J,i)) " Ai = A
thus  (proj (J,i)) " Ai = A by A4, WAYBEL18:4; ::_thesis: verum
end;

theorem Th17: :: YELLOW17:17
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
let i be Element of I; ::_thesis: for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
let xi be Element of (J . i); ::_thesis: for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
let A be set ; ::_thesis: ( A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) implies ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )
assume  A in product_prebasis J ; ::_thesis: ( not (proj (J,i)) " {xi} c= A or A = [#] (product J) or ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )
then consider i1 being Element of I, Ai1 being Subset of (J . i1) such that
A1: Ai1 is open and
A2: (proj (J,i1)) " Ai1 = A by Th16;
assume A3: (proj (J,i)) " {xi} c= A ; ::_thesis: ( A = [#] (product J) or ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )
assume  not A = [#] (product J) ; ::_thesis: ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
then A4: Ai1 <> [#] (J . i1) by A2, Th10;
then reconsider Ai = Ai1 as Subset of (J . i) by A3, A2, Th12;
take  Ai ; ::_thesis: ( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
thus  Ai <> [#] (J . i) by A3, A2, A4, Th12; ::_thesis: ( xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
thus  xi in Ai by A3, A2, A4, Th12; ::_thesis: ( Ai is open & A = (proj (J,i)) " Ai )
 J . i = J . i1 by A3, A2, A4, Th12;
hence  Ai is open by A1; ::_thesis: A = (proj (J,i)) " Ai
thus  A = (proj (J,i)) " Ai by A3, A2, A4, Th12; ::_thesis: verum
end;

theorem Th18: :: YELLOW17:18
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
let i be Element of I; ::_thesis: for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds
[#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
let Fi be non empty Subset-Family of (J . i); ::_thesis: ( [#] (J . i) c= union Fi implies [#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }  )
assume A1: [#] (J . i) c= union Fi ; ::_thesis: [#] (product J) c= union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in [#] (product J) or f in union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }  )
assume A2: f in [#] (product J) ; ::_thesis: f in union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }
then reconsider f9 = f as Element of (product J) ;
 f9 . i in [#] (J . i) ;
then consider Ai0 being set  such that
A3: f9 . i in Ai0 and
A4: Ai0 in Fi by A1, TARSKI:def_4;
 f9 in product (Carrier J) by A2, WAYBEL18:def_3;
then  f9 in dom (proj ((Carrier J),i)) by CARD_3:def_16;
then A5: f9 in dom (proj (J,i)) by WAYBEL18:def_4;
reconsider Ai0 = Ai0 as Element of Fi by A4;
 (proj (J,i)) . f9 in Ai0 by A3, Th8;
then  ( (proj (J,i)) " Ai0 in  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }  & f9 in (proj (J,i)) " Ai0 ) by A5, FUNCT_1:def_7;
hence  f in union  {  ((proj (J,i)) " Ai) where Ai is Element of Fi : verum  }  by TARSKI:def_4; ::_thesis: verum
end;

theorem Th19: :: YELLOW17:19
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G
let i be Element of I; ::_thesis: for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G
let xi be Element of (J . i); ::_thesis: for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G
let G be Subset of (product_prebasis J); ::_thesis: ( (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) implies [#] (product J) c= union G )
assume that
A1: (proj (J,i)) " {xi} c= union G and
A2: for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ; ::_thesis: [#] (product J) c= union G
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in [#] (product J) or f in union G )
assume  f in [#] (product J) ; ::_thesis: f in union G
then reconsider f9 = f as Element of (product J) ;
set g = f9 +* (i,xi);
A3: f9 +* (i,xi) in (proj (J,i)) " {xi} by Th11;
then consider Ag being set  such that
A4: f9 +* (i,xi) in Ag and
A5: Ag in G by A1, TARSKI:def_4;
consider i2 being Element of I, Ai2 being Subset of (J . i2) such that
 Ai2 is open and
A6: (proj (J,i2)) " Ai2 = Ag by A5, Th16;
A7: Ai2 <> [#] (J . i2)
proof
assume  Ai2 = [#] (J . i2) ; ::_thesis: contradiction
then (proj (J,i2)) " Ai2 = [#] (product J) by Th10
.= the carrier of (product J) ;
hence  contradiction by A2, A5, A6; ::_thesis: verum
end;
A8: not (proj (J,i)) " {xi} c= (proj (J,i2)) " Ai2 by A2, A5, A6;
 i <> i2
proof
assume A9: i = i2 ; ::_thesis: contradiction
then reconsider Ai29 = Ai2 as Subset of (J . i) ;
 ((proj (J,i)) " {xi}) /\ ((proj (J,i)) " Ai29) <> {} by A3, A4, A6, A9, XBOOLE_0:def_4;
then A10: (proj (J,i)) " {xi} meets (proj (J,i)) " Ai29 by XBOOLE_0:def_7;
 not xi in Ai2 by A8, A7, A9, Th12;
hence  contradiction by A10, Th9; ::_thesis: verum
end;
then  f in (proj (J,i2)) " Ai2 by A4, A6, Th13;
hence  f in union G by A5, A6, TARSKI:def_4; ::_thesis: verum
end;

theorem Th20: :: YELLOW17:20
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
let i be Element of I; ::_thesis: for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
let F be Subset of (product_prebasis J); ::_thesis: ( ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A ) )
assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; ::_thesis: for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
let xi be Element of (J . i); ::_thesis: for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
let G be finite Subset of F; ::_thesis: ( (proj (J,i)) " {xi} c= union G implies ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A ) )
reconsider G9 = G as Subset of (product_prebasis J) by XBOOLE_1:1;
assume A2: (proj (J,i)) " {xi} c= union G ; ::_thesis: ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
assume  for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ; ::_thesis: contradiction
then  [#] (product J) c= union G9 by A2, Th19;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th21: :: YELLOW17:21
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let i be Element of I; ::_thesis: for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let F be Subset of (product_prebasis J); ::_thesis: ( ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; ::_thesis: for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let xi be Element of (J . i); ::_thesis: for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let G be finite Subset of F; ::_thesis: ( (proj (J,i)) " {xi} c= union G implies ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
assume  (proj (J,i)) " {xi} c= union G ; ::_thesis: ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
then consider A being set  such that
A2: A in product_prebasis J and
A3: A in G and
A4: (proj (J,i)) " {xi} c= A by A1, Th20;
 A <> [#] (product J)
proof
reconsider G1 = {A} as finite Subset of F by A3, ZFMISC_1:31;
assume  A = [#] (product J) ; ::_thesis: contradiction
then  union G1 = [#] (product J) by ZFMISC_1:25;
hence  contradiction by A1; ::_thesis: verum
end;
then consider Ai being Subset of (J . i) such that
A5: Ai <> [#] (J . i) and
A6: xi in Ai and
A7: Ai is open and
A8: A = (proj (J,i)) " Ai by A2, A4, Th17;
take  Ai ; ::_thesis: ( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus  Ai <> [#] (J . i) by A5; ::_thesis: ( xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus  xi in Ai by A6; ::_thesis: ( (proj (J,i)) " Ai in G & Ai is open )
thus  (proj (J,i)) " Ai in G by A3, A8; ::_thesis: Ai is open
thus  Ai is open by A7; ::_thesis: verum
end;

theorem Th22: :: YELLOW17:22
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G
proof
defpred S1[ set ] means verum;
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G
let i be Element of I; ::_thesis: for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G
let F be Subset of (product_prebasis J); ::_thesis: ( ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G )
assume that
A1: for i being Element of I holds J . i is compact and
A2: for G being finite Subset of F holds not [#] (product J) c= union G ; ::_thesis: ex xi being Element of (J . i) st
for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G
deffunc H1( set ) ->  Element of bool the carrier of (product J) = (proj (J,i)) " $1;
defpred S2[ set , set ] means ( $1 in $2 & (proj (J,i)) " $2 in F & ( for V being Subset of (J . i) st V = $2 holds
V is open ) );
assume A3: for xi being Element of (J . i) ex G being finite Subset of F st (proj (J,i)) " {xi} c= union G ; ::_thesis: contradiction
A4: for xi being set st xi in the carrier of (J . i) holds
ex Ai being set st
( Ai in bool the carrier of (J . i) & S2[xi,Ai] )
proof
let xi be set ; ::_thesis: ( xi in the carrier of (J . i) implies ex Ai being set st
( Ai in bool the carrier of (J . i) & S2[xi,Ai] ) )
assume  xi in the carrier of (J . i) ; ::_thesis: ex Ai being set st
( Ai in bool the carrier of (J . i) & S2[xi,Ai] )
then reconsider xi9 = xi as Element of (J . i) ;
consider G being finite Subset of F such that
A5: (proj (J,i)) " {xi9} c= union G by A3;
consider Ai being Subset of (J . i) such that
 Ai <> [#] (J . i) and
A6: xi in Ai and
A7: (proj (J,i)) " Ai in G and
A8: Ai is open by A2, A5, Th21;
take  Ai ; ::_thesis: ( Ai in bool the carrier of (J . i) & S2[xi,Ai] )
thus  Ai in bool the carrier of (J . i) ; ::_thesis: S2[xi,Ai]
thus  xi in Ai by A6; ::_thesis: ( (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds
V is open ) )
thus  (proj (J,i)) " Ai in F by A7; ::_thesis: for V being Subset of (J . i) st V = Ai holds
V is open
let V be Subset of (J . i); ::_thesis: ( V = Ai implies V is open )
assume  V = Ai ; ::_thesis: V is open
hence  V is open by A8; ::_thesis: verum
end;
consider h being Function such that
A9: dom h = the carrier of (J . i) and
A10: rng h c= bool the carrier of (J . i) and
A11: for xi being set st xi in the carrier of (J . i) holds
S2[xi,h . xi] from FUNCT_1:sch_5(A4);
reconsider bGip = rng h as Subset-Family of (J . i) by A10;
reconsider bGip = bGip as Subset-Family of (J . i) ;
A12: [#] (J . i) c= union bGip
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (J . i) or x in union bGip )
assume  x in [#] (J . i) ; ::_thesis: x in union bGip
then  ( x in h . x & h . x in bGip ) by A9, A11, FUNCT_1:def_3;
hence  x in union bGip by TARSKI:def_4; ::_thesis: verum
end;
 for P being Subset of (J . i) st P in bGip holds
P is open
proof
let P be Subset of (J . i); ::_thesis: ( P in bGip implies P is open )
assume  P in bGip ; ::_thesis: P is open
then  ex x being set st
( x in dom h & P = h . x ) by FUNCT_1:def_3;
hence  P is open by A9, A11; ::_thesis: verum
end;
then A13: bGip is open by TOPS_2:def_1;
 J . i is compact by A1;
then consider Gip being Subset-Family of (J . i) such that
A14: Gip c= bGip and
A15: [#] (J . i) c= union Gip and
A16: Gip is finite by A12, A13, Th14;
reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by A15, A16, ZFMISC_1:2;
set Gp =  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  ;
A17:  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  c= F
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  or A in F )
assume  A in  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  ; ::_thesis: A in F
then consider Ai being Element of Gip such that
A18: A = (proj (J,i)) " Ai ;
 Ai in Gip ;
then  ex x being set st
( x in dom h & h . x = Ai ) by A14, FUNCT_1:def_3;
hence  A in F by A9, A11, A18; ::_thesis: verum
end;
  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  is finite from PRE_CIRC:sch_1();
then reconsider Gp =  {  H1(Ai) where Ai is Element of Gip : S1[Ai]  }  as finite Subset of F by A17;
 [#] (product J) c= union Gp by A15, Th18;
hence  contradiction by A2; ::_thesis: verum
end;

theorem :: YELLOW17:23
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds
product J is compact
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds
product J is compact
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is compact ) implies product J is compact )
assume A1: for i being Element of I holds J . i is compact ; ::_thesis: product J is compact
reconsider B = product_prebasis J as prebasis of (product J) by WAYBEL18:def_3;
assume  not product J is compact ; ::_thesis: contradiction
then consider F being Subset of B such that
A2: [#] (product J) c= union F and
A3: for G being finite Subset of F holds not [#] (product J) c= union G by Th15;
defpred S1[ set , Element of I] means  for G being finite Subset of F holds not (proj (J,$2)) " {$1} c= union G;
A4: for i being Element of I ex xi being Element of (J . i) st S1[xi,i] by A1, A3, Th22;
consider f being Element of (product J) such that
A5: for i being Element of I holds S1[f . i,i] from YELLOW17:sch_1(A4);
 f in [#] (product J) ;
then consider A being set  such that
A6: f in A and
A7: A in F by A2, TARSKI:def_4;
reconsider G = {A} as finite Subset of F by A7, ZFMISC_1:31;
consider i being Element of I, Ai being Subset of (J . i) such that
 Ai is open and
A8: (proj (J,i)) " Ai = A by A7, Th16;
 (proj (J,i)) . f in Ai by A6, A8, FUNCT_1:def_7;
then  f . i in Ai by Th8;
then  {(f . i)} c= Ai by ZFMISC_1:31;
then  (proj (J,i)) " {(f . i)} c= A by A8, RELAT_1:143;
then  (proj (J,i)) " {(f . i)} c= union G by ZFMISC_1:25;
hence  contradiction by A5; ::_thesis: verum
end;