let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

let P be Subset of (product (Carrier J)); :: thesis: ( P in FinMeetCl (product_prebasis J) implies ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) ) )

assume A1: P in FinMeetCl (product_prebasis J) ; :: thesis: ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

consider Y being Subset-Family of (product (Carrier J)) such that

A2: ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A1, CANTOR_1:def 3;

for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

let P be Subset of (product (Carrier J)); :: thesis: ( P in FinMeetCl (product_prebasis J) implies ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) ) )

assume A1: P in FinMeetCl (product_prebasis J) ; :: thesis: ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

consider Y being Subset-Family of (product (Carrier J)) such that

A2: ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A1, CANTOR_1:def 3;

per cases
( ( not Y is empty & meet Y <> {} ) or Y is empty or ( not Y is empty & meet Y = {} ) )
;

end;

suppose A3:
( not Y is empty & meet Y <> {} )
; :: thesis: ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

then A4:
P = meet Y
by A2, SETFAM_1:def 9;

defpred S_{1}[ object , object ] means ex i being Element of I ex B being Subset of (J . i) st

( $2 = i & B is open & $1 = product ((Carrier J) +* (i,B)) );

A5: for x being object st x in Y holds

ex i being object st

( i in I & S_{1}[x,i] )

A7: for x being object st x in Y holds

S_{1}[x,g . x]
from FUNCT_2:sch 1(A5);

set X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ;

{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } c= bool (product (Carrier J))

take X ; :: thesis: ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

defpred S_{2}[ object , object ] means ex i being Element of I st

( $2 = i & $1 = meet (g " {i}) & g " {i} <> {} );

A9: for x being object st x in X holds

ex i being object st

( i in I & S_{2}[x,i] )

A11: for x being object st x in X holds

S_{2}[x,f . x]
from FUNCT_2:sch 1(A9);

A12: ( dom f = X & rng f c= I ) by FUNCT_2:def 1;

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

take f ; :: thesis: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

A16: for i being Element of I

for S being non empty set st g " {i} <> {} & S in g " {i} holds

ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

ex Z being Subset-Family of (J . (In ((f . x),I))) st

( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

x in product_prebasis J

for x being object holds

( x in meet X iff x in meet Y )

thus X is finite :: thesis: ( P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

thus dom f = X by FUNCT_2:def 1; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,f)))

set F = (Carrier J) +* (product_basis_selector (J,f));

for x being object holds

( x in meet X iff x in product ((Carrier J) +* (product_basis_selector (J,f))) )

end;defpred S

( $2 = i & B is open & $1 = product ((Carrier J) +* (i,B)) );

A5: for x being object st x in Y holds

ex i being object st

( i in I & S

proof

consider g being Function of Y,I such that
let x be object ; :: thesis: ( x in Y implies ex i being object st

( i in I & S_{1}[x,i] ) )

assume x in Y ; :: thesis: ex i being object st

( i in I & S_{1}[x,i] )

then consider i being set , T being TopStruct , V being Subset of T such that

A6: ( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) by A2, WAYBEL18:def 2;

take i ; :: thesis: ( i in I & S_{1}[x,i] )

thus i in I by A6; :: thesis: S_{1}[x,i]

reconsider j = i as Element of I by A6;

reconsider V = V as Subset of (J . j) by A6;

take j ; :: thesis: ex B being Subset of (J . j) st

( i = j & B is open & x = product ((Carrier J) +* (j,B)) )

take V ; :: thesis: ( i = j & V is open & x = product ((Carrier J) +* (j,V)) )

thus ( i = j & V is open & x = product ((Carrier J) +* (j,V)) ) by A6; :: thesis: verum

end;( i in I & S

assume x in Y ; :: thesis: ex i being object st

( i in I & S

then consider i being set , T being TopStruct , V being Subset of T such that

A6: ( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) by A2, WAYBEL18:def 2;

take i ; :: thesis: ( i in I & S

thus i in I by A6; :: thesis: S

reconsider j = i as Element of I by A6;

reconsider V = V as Subset of (J . j) by A6;

take j ; :: thesis: ex B being Subset of (J . j) st

( i = j & B is open & x = product ((Carrier J) +* (j,B)) )

take V ; :: thesis: ( i = j & V is open & x = product ((Carrier J) +* (j,V)) )

thus ( i = j & V is open & x = product ((Carrier J) +* (j,V)) ) by A6; :: thesis: verum

A7: for x being object st x in Y holds

S

set X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ;

{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } c= bool (product (Carrier J))

proof

then reconsider X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } as Subset-Family of (product (Carrier J)) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } or x in bool (product (Carrier J)) )

assume x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ; :: thesis: x in bool (product (Carrier J))

then consider i being Element of I such that

A8: ( x = meet (g " {i}) & g " {i} <> {} ) ;

reconsider Z = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;

meet Z is Subset of (product (Carrier J)) ;

hence x in bool (product (Carrier J)) by A8; :: thesis: verum

end;assume x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ; :: thesis: x in bool (product (Carrier J))

then consider i being Element of I such that

A8: ( x = meet (g " {i}) & g " {i} <> {} ) ;

reconsider Z = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;

meet Z is Subset of (product (Carrier J)) ;

hence x in bool (product (Carrier J)) by A8; :: thesis: verum

take X ; :: thesis: ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

defpred S

( $2 = i & $1 = meet (g " {i}) & g " {i} <> {} );

A9: for x being object st x in X holds

ex i being object st

( i in I & S

proof

consider f being Function of X,I such that
let x be object ; :: thesis: ( x in X implies ex i being object st

( i in I & S_{2}[x,i] ) )

assume x in X ; :: thesis: ex i being object st

( i in I & S_{2}[x,i] )

then consider i being Element of I such that

A10: ( x = meet (g " {i}) & g " {i} <> {} ) ;

take i ; :: thesis: ( i in I & S_{2}[x,i] )

thus i in I ; :: thesis: S_{2}[x,i]

take i ; :: thesis: ( i = i & x = meet (g " {i}) & g " {i} <> {} )

thus ( i = i & x = meet (g " {i}) & g " {i} <> {} ) by A10; :: thesis: verum

end;( i in I & S

assume x in X ; :: thesis: ex i being object st

( i in I & S

then consider i being Element of I such that

A10: ( x = meet (g " {i}) & g " {i} <> {} ) ;

take i ; :: thesis: ( i in I & S

thus i in I ; :: thesis: S

take i ; :: thesis: ( i = i & x = meet (g " {i}) & g " {i} <> {} )

thus ( i = i & x = meet (g " {i}) & g " {i} <> {} ) by A10; :: thesis: verum

A11: for x being object st x in X holds

S

A12: ( dom f = X & rng f c= I ) by FUNCT_2:def 1;

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

proof

then reconsider f = f as I -valued one-to-one Function by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

then consider i1 being Element of I such that

A14: ( f . x1 = i1 & x1 = meet (g " {i1}) & g " {i1} <> {} ) by A11;

ex i2 being Element of I st

( f . x2 = i2 & x2 = meet (g " {i2}) & g " {i2} <> {} ) by A11, A13;

hence x1 = x2 by A13, A14; :: thesis: verum

end;assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

then consider i1 being Element of I such that

A14: ( f . x1 = i1 & x1 = meet (g " {i1}) & g " {i1} <> {} ) by A11;

ex i2 being Element of I st

( f . x2 = i2 & x2 = meet (g " {i2}) & g " {i2} <> {} ) by A11, A13;

hence x1 = x2 by A13, A14; :: thesis: verum

take f ; :: thesis: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

A16: for i being Element of I

for S being non empty set st g " {i} <> {} & S in g " {i} holds

ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

proof

A27:
not X is empty
let i be Element of I; :: thesis: for S being non empty set st g " {i} <> {} & S in g " {i} holds

ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

let S be non empty set ; :: thesis: ( g " {i} <> {} & S in g " {i} implies ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V)) )

assume a17: ( g " {i} <> {} & S in g " {i} ) ; :: thesis: ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

then A17: ( S in Y & g . S in {i} ) by FUNCT_2:38;

then consider j being set , T being TopStruct , V being Subset of T such that

A18: ( j in I & V is open & T = J . j ) and

A19: S = product ((Carrier J) +* (j,V)) by A2, WAYBEL18:def 2;

a20: dom (Carrier J) = I by PARTFUN1:def 2;

end;ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

let S be non empty set ; :: thesis: ( g " {i} <> {} & S in g " {i} implies ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V)) )

assume a17: ( g " {i} <> {} & S in g " {i} ) ; :: thesis: ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

then A17: ( S in Y & g . S in {i} ) by FUNCT_2:38;

then consider j being set , T being TopStruct , V being Subset of T such that

A18: ( j in I & V is open & T = J . j ) and

A19: S = product ((Carrier J) +* (j,V)) by A2, WAYBEL18:def 2;

a20: dom (Carrier J) = I by PARTFUN1:def 2;

per cases
( V <> (Carrier J) . j or V = (Carrier J) . j )
;

end;

suppose A21:
V <> (Carrier J) . j
; :: thesis: ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

A22:
not V is empty
by A19, a20, Th36, A18;

A23: i = j

take V ; :: thesis: S = product ((Carrier J) +* (i,V))

thus S = product ((Carrier J) +* (i,V)) by A19, A23; :: thesis: verum

end;A23: i = j

proof

then reconsider V = V as non empty open Subset of (J . i) by A19, a20, Th36, A18;
g . S = i
by A17, TARSKI:def 1;

then consider k being Element of I, B being Subset of (J . k) such that

A24: ( i = k & B is open ) and

A25: S = product ((Carrier J) +* (k,B)) by A7, a17;

not B is empty by a20, A25, Th36;

hence i = j by A19, A18, a20, A21, A22, A24, A25, Th42; :: thesis: verum

end;then consider k being Element of I, B being Subset of (J . k) such that

A24: ( i = k & B is open ) and

A25: S = product ((Carrier J) +* (k,B)) by A7, a17;

not B is empty by a20, A25, Th36;

hence i = j by A19, A18, a20, A21, A22, A24, A25, Th42; :: thesis: verum

take V ; :: thesis: S = product ((Carrier J) +* (i,V))

thus S = product ((Carrier J) +* (i,V)) by A19, A23; :: thesis: verum

suppose
V = (Carrier J) . j
; :: thesis: ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

then A26: S =
product (Carrier J)
by A19, FUNCT_7:35

.= product ((Carrier J) +* (i,((Carrier J) . i))) by FUNCT_7:35 ;

take [#] (J . i) ; :: thesis: S = product ((Carrier J) +* (i,([#] (J . i))))

thus S = product ((Carrier J) +* (i,([#] (J . i)))) by A26, PENCIL_3:7; :: thesis: verum

end;.= product ((Carrier J) +* (i,((Carrier J) . i))) by FUNCT_7:35 ;

take [#] (J . i) ; :: thesis: S = product ((Carrier J) +* (i,([#] (J . i))))

thus S = product ((Carrier J) +* (i,([#] (J . i)))) by A26, PENCIL_3:7; :: thesis: verum

proof

A31:
for x being Element of X st x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} holds
A28:
ex i being Element of I st g " {i} <> {}

end;proof

ex x being object st x in X
set A = the Element of Y;

consider i being Element of I, B being Subset of (J . i) such that

A29: ( g . the Element of Y = i & B is open & the Element of Y = product ((Carrier J) +* (i,B)) ) by A3, A7;

take i ; :: thesis: g " {i} <> {}

g . the Element of Y in {i} by A29, TARSKI:def 1;

hence g " {i} <> {} by A3, FUNCT_2:38; :: thesis: verum

end;consider i being Element of I, B being Subset of (J . i) such that

A29: ( g . the Element of Y = i & B is open & the Element of Y = product ((Carrier J) +* (i,B)) ) by A3, A7;

take i ; :: thesis: g " {i} <> {}

g . the Element of Y in {i} by A29, TARSKI:def 1;

hence g " {i} <> {} by A3, FUNCT_2:38; :: thesis: verum

proof

hence
not X is empty
; :: thesis: verum
consider i being Element of I such that

A30: g " {i} <> {} by A28;

meet (g " {i}) in X by A30;

hence ex x being object st x in X ; :: thesis: verum

end;A30: g " {i} <> {} by A28;

meet (g " {i}) in X by A30;

hence ex x being object st x in X ; :: thesis: verum

ex Z being Subset-Family of (J . (In ((f . x),I))) st

( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

proof

for x being object st x in X holds
let x be Element of X; :: thesis: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} implies ex Z being Subset-Family of (J . (In ((f . x),I))) st

( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) ) )

set i = In ((f . x),I);

a32: f . x in rng f by A12, A27, FUNCT_1:3;

then A32: In ((f . x),I) = f . x by SUBSET_1:def 8;

assume A33: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} ) ; :: thesis: ex Z being Subset-Family of (J . (In ((f . x),I))) st

( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

set Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ;

{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } c= bool the carrier of (J . (In ((f . x),I)))

take Z ; :: thesis: ( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

thus Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis: ( Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

for A being Subset of (J . (In ((f . x),I))) st A in Z holds

A is open

defpred S_{3}[ object , object ] means ex V being Subset of (product (Carrier J)) st

( $1 = V & $2 = (proj (J,(In ((f . x),I)))) .: V );

A37: for y, z1, z2 being object st y in g " {(In ((f . x),I))} & S_{3}[y,z1] & S_{3}[y,z2] holds

z1 = z2 ;

A38: for y being object st y in g " {(In ((f . x),I))} holds

ex z being object st S_{3}[y,z]

A39: ( dom h = g " {(In ((f . x),I))} & ( for y being object st y in g " {(In ((f . x),I))} holds

S_{3}[y,h . y] ) )
from FUNCT_1:sch 2(A37, A38);

a45: for y being object holds

( y in rng h iff y in Z )

hence Z is finite by A2, A39, FINSET_1:8; :: thesis: ( not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

h . the Element of g " {(f . x)} in rng h by A32, A33, A39, FUNCT_1:3;

hence A46: not Z is empty by a45; :: thesis: x = product ((Carrier J) +* ((f . x),(meet Z)))

a47: dom (Carrier J) = I by PARTFUN1:def 2;

then A47: In ((f . x),I) in dom (Carrier J) ;

for y being object holds

( y in meet (g " {(In ((f . x),I))}) iff y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )

end;( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) ) )

set i = In ((f . x),I);

a32: f . x in rng f by A12, A27, FUNCT_1:3;

then A32: In ((f . x),I) = f . x by SUBSET_1:def 8;

assume A33: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} ) ; :: thesis: ex Z being Subset-Family of (J . (In ((f . x),I))) st

( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

set Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ;

{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } c= bool the carrier of (J . (In ((f . x),I)))

proof

then reconsider Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } as Subset-Family of (J . (In ((f . x),I))) ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } or y in bool the carrier of (J . (In ((f . x),I))) )

assume y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis: y in bool the carrier of (J . (In ((f . x),I)))

then ex V being Subset of (product (Carrier J)) st

( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

hence y in bool the carrier of (J . (In ((f . x),I))) ; :: thesis: verum

end;assume y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis: y in bool the carrier of (J . (In ((f . x),I)))

then ex V being Subset of (product (Carrier J)) st

( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

hence y in bool the carrier of (J . (In ((f . x),I))) ; :: thesis: verum

take Z ; :: thesis: ( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

thus Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis: ( Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

for A being Subset of (J . (In ((f . x),I))) st A in Z holds

A is open

proof

hence
Z is open
by TOPS_2:def 1; :: thesis: ( Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
let A be Subset of (J . (In ((f . x),I))); :: thesis: ( A in Z implies A is open )

assume A in Z ; :: thesis: A is open

then consider V being Subset of (product (Carrier J)) such that

A35: ( A = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

( V in Y & ( V is empty or not V is empty ) ) by A35;

hence A is open by A2, A35, Th58; :: thesis: verum

end;assume A in Z ; :: thesis: A is open

then consider V being Subset of (product (Carrier J)) such that

A35: ( A = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

( V in Y & ( V is empty or not V is empty ) ) by A35;

hence A is open by A2, A35, Th58; :: thesis: verum

defpred S

( $1 = V & $2 = (proj (J,(In ((f . x),I)))) .: V );

A37: for y, z1, z2 being object st y in g " {(In ((f . x),I))} & S

z1 = z2 ;

A38: for y being object st y in g " {(In ((f . x),I))} holds

ex z being object st S

proof

consider h being Function such that
let y be object ; :: thesis: ( y in g " {(In ((f . x),I))} implies ex z being object st S_{3}[y,z] )

assume y in g " {(In ((f . x),I))} ; :: thesis: ex z being object st S_{3}[y,z]

then y in Y ;

then reconsider V = y as Subset of (product (Carrier J)) ;

take (proj (J,(In ((f . x),I)))) .: V ; :: thesis: S_{3}[y,(proj (J,(In ((f . x),I)))) .: V]

take V ; :: thesis: ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V )

thus ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V ) ; :: thesis: verum

end;assume y in g " {(In ((f . x),I))} ; :: thesis: ex z being object st S

then y in Y ;

then reconsider V = y as Subset of (product (Carrier J)) ;

take (proj (J,(In ((f . x),I)))) .: V ; :: thesis: S

take V ; :: thesis: ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V )

thus ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V ) ; :: thesis: verum

A39: ( dom h = g " {(In ((f . x),I))} & ( for y being object st y in g " {(In ((f . x),I))} holds

S

a45: for y being object holds

( y in rng h iff y in Z )

proof

then
rng h = Z
by TARSKI:2;
let y be object ; :: thesis: ( y in rng h iff y in Z )

then consider V being Subset of (product (Carrier J)) such that

A42: ( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

A43: V in dom h by a32, SUBSET_1:def 8, A39, A42;

ex V0 being Subset of (product (Carrier J)) st

( V = V0 & h . V = (proj (J,(In ((f . x),I)))) .: V0 ) by A32, A39, A42;

hence y in rng h by A42, A43, FUNCT_1:def 3; :: thesis: verum

end;hereby :: thesis: ( y in Z implies y in rng h )

assume
y in Z
; :: thesis: y in rng hassume
y in rng h
; :: thesis: y in Z

then consider z being object such that

A40: ( z in dom h & y = h . z ) by FUNCT_1:def 3;

ex V being Subset of (product (Carrier J)) st

( z = V & h . z = (proj (J,(In ((f . x),I)))) .: V ) by A39, A40;

hence y in Z by A32, A39, A40; :: thesis: verum

end;then consider z being object such that

A40: ( z in dom h & y = h . z ) by FUNCT_1:def 3;

ex V being Subset of (product (Carrier J)) st

( z = V & h . z = (proj (J,(In ((f . x),I)))) .: V ) by A39, A40;

hence y in Z by A32, A39, A40; :: thesis: verum

then consider V being Subset of (product (Carrier J)) such that

A42: ( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;

A43: V in dom h by a32, SUBSET_1:def 8, A39, A42;

ex V0 being Subset of (product (Carrier J)) st

( V = V0 & h . V = (proj (J,(In ((f . x),I)))) .: V0 ) by A32, A39, A42;

hence y in rng h by A42, A43, FUNCT_1:def 3; :: thesis: verum

hence Z is finite by A2, A39, FINSET_1:8; :: thesis: ( not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

h . the Element of g " {(f . x)} in rng h by A32, A33, A39, FUNCT_1:3;

hence A46: not Z is empty by a45; :: thesis: x = product ((Carrier J) +* ((f . x),(meet Z)))

a47: dom (Carrier J) = I by PARTFUN1:def 2;

then A47: In ((f . x),I) in dom (Carrier J) ;

for y being object holds

( y in meet (g " {(In ((f . x),I))}) iff y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )

proof

hence
x = product ((Carrier J) +* ((f . x),(meet Z)))
by A32, A33, TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in meet (g " {(In ((f . x),I))}) iff y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )

for S being set st S in g " {(In ((f . x),I))} holds

y in S

end;hereby :: thesis: ( y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) implies y in meet (g " {(In ((f . x),I))}) )

assume A64:
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
; :: thesis: y in meet (g " {(In ((f . x),I))})assume A49:
y in meet (g " {(In ((f . x),I))})
; :: thesis: y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))

set S0 = the Element of g " {(In ((f . x),I))};

not the Element of g " {(In ((f . x),I))} is empty by A32, A33, A49, SETFAM_1:def 1;

then consider V0 being non empty open Subset of (J . (In ((f . x),I))) such that

A50: the Element of g " {(In ((f . x),I))} = product ((Carrier J) +* ((In ((f . x),I)),V0)) by A16, A32, A33;

y in product ((Carrier J) +* ((In ((f . x),I)),V0)) by A32, A33, A49, A50, SETFAM_1:def 1;

then consider f0 being Function such that

A51: ( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),V0)) ) and

A52: for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) holds

f0 . z in ((Carrier J) +* ((In ((f . x),I)),V0)) . z by CARD_3:def 5;

end;set S0 = the Element of g " {(In ((f . x),I))};

not the Element of g " {(In ((f . x),I))} is empty by A32, A33, A49, SETFAM_1:def 1;

then consider V0 being non empty open Subset of (J . (In ((f . x),I))) such that

A50: the Element of g " {(In ((f . x),I))} = product ((Carrier J) +* ((In ((f . x),I)),V0)) by A16, A32, A33;

y in product ((Carrier J) +* ((In ((f . x),I)),V0)) by A32, A33, A49, A50, SETFAM_1:def 1;

then consider f0 being Function such that

A51: ( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),V0)) ) and

A52: for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) holds

f0 . z in ((Carrier J) +* ((In ((f . x),I)),V0)) . z by CARD_3:def 5;

now :: thesis: ex f0 being Function st

( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z ) )

hence
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
by CARD_3:def 5; :: thesis: verum( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z ) )

take f0 = f0; :: thesis: ( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

b_{2} . b_{3} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{3} ) )

thus y = f0 by A51; :: thesis: ( dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

b_{2} . b_{3} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{3} ) )

thus dom f0 = dom (Carrier J) by A51, FUNCT_7:30

.= dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) by FUNCT_7:30 ; :: thesis: for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

b_{2} . b_{3} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{3}

let z be object ; :: thesis: ( z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) implies b_{1} . b_{2} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{2} )

assume z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) ; :: thesis: b_{1} . b_{2} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{2}

then A53: z in dom (Carrier J) by FUNCT_7:30;

end;b

thus y = f0 by A51; :: thesis: ( dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

b

thus dom f0 = dom (Carrier J) by A51, FUNCT_7:30

.= dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) by FUNCT_7:30 ; :: thesis: for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds

b

let z be object ; :: thesis: ( z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) implies b

assume z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) ; :: thesis: b

then A53: z in dom (Carrier J) by FUNCT_7:30;

per cases
( z <> In ((f . x),I) or z = In ((f . x),I) )
;

end;

suppose A54:
z <> In ((f . x),I)
; :: thesis: b_{1} . b_{2} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{2}

then A55: ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z =
(Carrier J) . z
by FUNCT_7:32

.= ((Carrier J) +* ((In ((f . x),I)),V0)) . z by A54, FUNCT_7:32 ;

z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) by A53, FUNCT_7:30;

hence f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z by A52, A55; :: thesis: verum

end;.= ((Carrier J) +* ((In ((f . x),I)),V0)) . z by A54, FUNCT_7:32 ;

z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) by A53, FUNCT_7:30;

hence f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z by A52, A55; :: thesis: verum

suppose A56:
z = In ((f . x),I)
; :: thesis: b_{1} . b_{2} in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b_{2}

then A57:
((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z = meet Z
by A53, FUNCT_7:31;

for S being set st S in Z holds

f0 . z in S

end;for S being set st S in Z holds

f0 . z in S

proof

hence
f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z
by A57, A46, SETFAM_1:def 1; :: thesis: verum
let S be set ; :: thesis: ( S in Z implies f0 . z in S )

assume S in Z ; :: thesis: f0 . z in S

then consider S1 being Subset of (product (Carrier J)) such that

A58: ( S = (proj (J,(In ((f . x),I)))) .: S1 & S1 in g " {(f . x)} ) ;

not S1 is empty by A32, A49, A58, SETFAM_1:def 1;

then consider V1 being non empty open Subset of (J . (In ((f . x),I))) such that

A59: S1 = product ((Carrier J) +* ((In ((f . x),I)),V1)) by A16, A32, A58;

V1 c= the carrier of (J . (In ((f . x),I))) ;

then V1 c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;

then A60: V1 c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;

proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;

then A61: S = V1 by A58, A59, A60, a47, Th43;

y in S1 by A32, A49, A58, SETFAM_1:def 1;

then consider f1 being Function such that

A62: ( y = f1 & dom f1 = dom ((Carrier J) +* ((In ((f . x),I)),V1)) ) and

A63: for a being object st a in dom ((Carrier J) +* ((In ((f . x),I)),V1)) holds

f1 . a in ((Carrier J) +* ((In ((f . x),I)),V1)) . a by A59, CARD_3:def 5;

In ((f . x),I) in dom ((Carrier J) +* ((In ((f . x),I)),V1)) by A47, FUNCT_7:30;

then f1 . (In ((f . x),I)) in ((Carrier J) +* ((In ((f . x),I)),V1)) . (In ((f . x),I)) by A63;

hence f0 . z in S by A51, A56, A61, A62, a47, FUNCT_7:31; :: thesis: verum

end;assume S in Z ; :: thesis: f0 . z in S

then consider S1 being Subset of (product (Carrier J)) such that

A58: ( S = (proj (J,(In ((f . x),I)))) .: S1 & S1 in g " {(f . x)} ) ;

not S1 is empty by A32, A49, A58, SETFAM_1:def 1;

then consider V1 being non empty open Subset of (J . (In ((f . x),I))) such that

A59: S1 = product ((Carrier J) +* ((In ((f . x),I)),V1)) by A16, A32, A58;

V1 c= the carrier of (J . (In ((f . x),I))) ;

then V1 c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;

then A60: V1 c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;

proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;

then A61: S = V1 by A58, A59, A60, a47, Th43;

y in S1 by A32, A49, A58, SETFAM_1:def 1;

then consider f1 being Function such that

A62: ( y = f1 & dom f1 = dom ((Carrier J) +* ((In ((f . x),I)),V1)) ) and

A63: for a being object st a in dom ((Carrier J) +* ((In ((f . x),I)),V1)) holds

f1 . a in ((Carrier J) +* ((In ((f . x),I)),V1)) . a by A59, CARD_3:def 5;

In ((f . x),I) in dom ((Carrier J) +* ((In ((f . x),I)),V1)) by A47, FUNCT_7:30;

then f1 . (In ((f . x),I)) in ((Carrier J) +* ((In ((f . x),I)),V1)) . (In ((f . x),I)) by A63;

hence f0 . z in S by A51, A56, A61, A62, a47, FUNCT_7:31; :: thesis: verum

for S being set st S in g " {(In ((f . x),I))} holds

y in S

proof

hence
y in meet (g " {(In ((f . x),I))})
by A32, A33, SETFAM_1:def 1; :: thesis: verum
let S be set ; :: thesis: ( S in g " {(In ((f . x),I))} implies y in S )

assume A65: S in g " {(In ((f . x),I))} ; :: thesis: y in S

not S is empty by A32, A33, A65, SETFAM_1:4;

then consider V being non empty open Subset of (J . (In ((f . x),I))) such that

A66: S = product ((Carrier J) +* ((In ((f . x),I)),V)) by A16, A65;

V c= the carrier of (J . (In ((f . x),I))) ;

then V c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;

then A67: V c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;

proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;

then A68: (proj (J,(In ((f . x),I)))) .: S = V by a47, A66, A67, Th43;

S in Y by A65;

then V in Z by A32, A65, A68;

then product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) c= product ((Carrier J) +* ((In ((f . x),I)),V)) by a47, Th38, SETFAM_1:3;

hence y in S by A64, A66; :: thesis: verum

end;assume A65: S in g " {(In ((f . x),I))} ; :: thesis: y in S

not S is empty by A32, A33, A65, SETFAM_1:4;

then consider V being non empty open Subset of (J . (In ((f . x),I))) such that

A66: S = product ((Carrier J) +* ((In ((f . x),I)),V)) by A16, A65;

V c= the carrier of (J . (In ((f . x),I))) ;

then V c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;

then A67: V c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;

proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;

then A68: (proj (J,(In ((f . x),I)))) .: S = V by a47, A66, A67, Th43;

S in Y by A65;

then V in Z by A32, A65, A68;

then product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) c= product ((Carrier J) +* ((In ((f . x),I)),V)) by a47, Th38, SETFAM_1:3;

hence y in S by A64, A66; :: thesis: verum

x in product_prebasis J

proof

hence
X c= product_prebasis J
by TARSKI:def 3; :: thesis: ( X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
let x be object ; :: thesis: ( x in X implies x in product_prebasis J )

assume A69: x in X ; :: thesis: x in product_prebasis J

end;assume A69: x in X ; :: thesis: x in product_prebasis J

per cases
( x <> {} or x = {} )
;

end;

suppose A70:
x <> {}
; :: thesis: x in product_prebasis J

ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )

end;( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )

proof

hence
x in product_prebasis J
by A69, WAYBEL18:def 2; :: thesis: verum
consider i being Element of I such that

A71: ( f . x = i & x = meet (g " {i}) & g " {i} <> {} ) by A11, A69;

consider Z being Subset-Family of (J . (In ((f . x),I))) such that

Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } and

A72: ( Z is open & Z is finite & not Z is empty ) and

A73: x = product ((Carrier J) +* ((f . x),(meet Z))) by A31, A69, A70, A71;

set W = meet Z;

take i ; :: thesis: ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )

take J . (In ((f . x),I)) ; :: thesis: ex V being Subset of (J . (In ((f . x),I))) st

( i in I & V is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,V)) )

take meet Z ; :: thesis: ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) )

thus ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) ) by A71, A73, A72, TOPS_2:20; :: thesis: verum

end;A71: ( f . x = i & x = meet (g " {i}) & g " {i} <> {} ) by A11, A69;

consider Z being Subset-Family of (J . (In ((f . x),I))) such that

Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } and

A72: ( Z is open & Z is finite & not Z is empty ) and

A73: x = product ((Carrier J) +* ((f . x),(meet Z))) by A31, A69, A70, A71;

set W = meet Z;

take i ; :: thesis: ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )

take J . (In ((f . x),I)) ; :: thesis: ex V being Subset of (J . (In ((f . x),I))) st

( i in I & V is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,V)) )

take meet Z ; :: thesis: ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) )

thus ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) ) by A71, A73, A72, TOPS_2:20; :: thesis: verum

for x being object holds

( x in meet X iff x in meet Y )

proof

then A81:
meet X = meet Y
by TARSKI:2;
let x be object ; :: thesis: ( x in meet X iff x in meet Y )

for Sx being set st Sx in X holds

x in Sx

end;hereby :: thesis: ( x in meet Y implies x in meet X )

assume A79:
x in meet Y
; :: thesis: x in meet Xassume A74:
x in meet X
; :: thesis: x in meet Y

for Sy being set st Sy in Y holds

x in Sy

end;for Sy being set st Sy in Y holds

x in Sy

proof

hence
x in meet Y
by A3, SETFAM_1:def 1; :: thesis: verum
let Sy be set ; :: thesis: ( Sy in Y implies x in Sy )

assume A75: Sy in Y ; :: thesis: x in Sy

then consider i being Element of I, B being Subset of (J . i) such that

A76: ( g . Sy = i & B is open & Sy = product ((Carrier J) +* (i,B)) ) by A7;

g . Sy in {i} by A76, TARSKI:def 1;

then A77: Sy in g " {i} by A75, FUNCT_2:38;

then meet (g " {i}) in X ;

then A78: x in meet (g " {i}) by A74, SETFAM_1:def 1;

meet (g " {i}) c= Sy by A77, SETFAM_1:3;

hence x in Sy by A78; :: thesis: verum

end;assume A75: Sy in Y ; :: thesis: x in Sy

then consider i being Element of I, B being Subset of (J . i) such that

A76: ( g . Sy = i & B is open & Sy = product ((Carrier J) +* (i,B)) ) by A7;

g . Sy in {i} by A76, TARSKI:def 1;

then A77: Sy in g " {i} by A75, FUNCT_2:38;

then meet (g " {i}) in X ;

then A78: x in meet (g " {i}) by A74, SETFAM_1:def 1;

meet (g " {i}) c= Sy by A77, SETFAM_1:3;

hence x in Sy by A78; :: thesis: verum

for Sx being set st Sx in X holds

x in Sx

proof

hence
x in meet X
by A27, SETFAM_1:def 1; :: thesis: verum
let Sx be set ; :: thesis: ( Sx in X implies x in Sx )

assume Sx in X ; :: thesis: x in Sx

then consider i being Element of I such that

A80: ( Sx = meet (g " {i}) & g " {i} <> {} ) ;

for A being set st A in g " {i} holds

x in A by A79, SETFAM_1:def 1;

hence x in Sx by A80, SETFAM_1:def 1; :: thesis: verum

end;assume Sx in X ; :: thesis: x in Sx

then consider i being Element of I such that

A80: ( Sx = meet (g " {i}) & g " {i} <> {} ) ;

for A being set st A in g " {i} holds

x in A by A79, SETFAM_1:def 1;

hence x in Sx by A80, SETFAM_1:def 1; :: thesis: verum

thus X is finite :: thesis: ( P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

proof

thus
P = Intersect X
by A4, A27, A81, SETFAM_1:def 9; :: thesis: ( dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
set S = { (g " {i}) where i is Element of I : i in rng g } ;

a82: { (g " {i}) where i is Element of I : i in rng g } is a_partition of Y by Th5;

defpred S_{3}[ object , object ] means ex M being set st

( $1 = M & $2 = meet M );

A83: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds

ex B being object st

( B in X & S_{3}[A,B] )

A86: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds

S_{3}[A,h . A]
from FUNCT_2:sch 1(A83);

for B being object st B in X holds

ex A being object st

( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

hence X is finite by a82, A2; :: thesis: verum

end;a82: { (g " {i}) where i is Element of I : i in rng g } is a_partition of Y by Th5;

defpred S

( $1 = M & $2 = meet M );

A83: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds

ex B being object st

( B in X & S

proof

consider h being Function of { (g " {i}) where i is Element of I : i in rng g } ,X such that
let A be object ; :: thesis: ( A in { (g " {i}) where i is Element of I : i in rng g } implies ex B being object st

( B in X & S_{3}[A,B] ) )

assume A in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: ex B being object st

( B in X & S_{3}[A,B] )

then consider i being Element of I such that

A84: ( A = g " {i} & i in rng g ) ;

take meet (g " {i}) ; :: thesis: ( meet (g " {i}) in X & S_{3}[A, meet (g " {i})] )

consider x being object such that

A85: ( x in Y & g . x = i ) by A84, FUNCT_2:11;

i in {i} by TARSKI:def 1;

then x in g " {i} by A85, FUNCT_2:38;

hence meet (g " {i}) in X ; :: thesis: S_{3}[A, meet (g " {i})]

take g " {i} ; :: thesis: ( A = g " {i} & meet (g " {i}) = meet (g " {i}) )

thus ( A = g " {i} & meet (g " {i}) = meet (g " {i}) ) by A84; :: thesis: verum

end;( B in X & S

assume A in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: ex B being object st

( B in X & S

then consider i being Element of I such that

A84: ( A = g " {i} & i in rng g ) ;

take meet (g " {i}) ; :: thesis: ( meet (g " {i}) in X & S

consider x being object such that

A85: ( x in Y & g . x = i ) by A84, FUNCT_2:11;

i in {i} by TARSKI:def 1;

then x in g " {i} by A85, FUNCT_2:38;

hence meet (g " {i}) in X ; :: thesis: S

take g " {i} ; :: thesis: ( A = g " {i} & meet (g " {i}) = meet (g " {i}) )

thus ( A = g " {i} & meet (g " {i}) = meet (g " {i}) ) by A84; :: thesis: verum

A86: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds

S

for B being object st B in X holds

ex A being object st

( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

proof

then
rng h = X
by FUNCT_2:10;
let B be object ; :: thesis: ( B in X implies ex A being object st

( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A ) )

assume B in X ; :: thesis: ex A being object st

( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

then consider i being Element of I such that

A87: ( B = meet (g " {i}) & g " {i} <> {} ) ;

take g " {i} ; :: thesis: ( g " {i} in { (g " {i}) where i is Element of I : i in rng g } & B = h . (g " {i}) )

consider x being object such that

A88: x in g " {i} by A87, XBOOLE_0:def 1;

( x in Y & g . x in {i} ) by A88, FUNCT_2:38;

then A90: g . x = i by TARSKI:def 1;

dom g = Y by FUNCT_2:def 1;

then i in rng g by A88, A90, FUNCT_1:def 3;

hence g " {i} in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: B = h . (g " {i})

then ex M being set st

( g " {i} = M & h . (g " {i}) = meet M ) by A86;

hence B = h . (g " {i}) by A87; :: thesis: verum

end;( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A ) )

assume B in X ; :: thesis: ex A being object st

( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

then consider i being Element of I such that

A87: ( B = meet (g " {i}) & g " {i} <> {} ) ;

take g " {i} ; :: thesis: ( g " {i} in { (g " {i}) where i is Element of I : i in rng g } & B = h . (g " {i}) )

consider x being object such that

A88: x in g " {i} by A87, XBOOLE_0:def 1;

( x in Y & g . x in {i} ) by A88, FUNCT_2:38;

then A90: g . x = i by TARSKI:def 1;

dom g = Y by FUNCT_2:def 1;

then i in rng g by A88, A90, FUNCT_1:def 3;

hence g " {i} in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: B = h . (g " {i})

then ex M being set st

( g " {i} = M & h . (g " {i}) = meet M ) by A86;

hence B = h . (g " {i}) by A87; :: thesis: verum

hence X is finite by a82, A2; :: thesis: verum

thus dom f = X by FUNCT_2:def 1; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,f)))

set F = (Carrier J) +* (product_basis_selector (J,f));

for x being object holds

( x in meet X iff x in product ((Carrier J) +* (product_basis_selector (J,f))) )

proof

hence
P = product ((Carrier J) +* (product_basis_selector (J,f)))
by A4, A81, TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in meet X iff x in product ((Carrier J) +* (product_basis_selector (J,f))) )

A92: I = I \/ (rng f) by XBOOLE_1:12

.= (dom (Carrier J)) \/ (rng f) by PARTFUN1:def 2

.= (dom (Carrier J)) \/ (dom (product_basis_selector (J,f))) by PARTFUN1:def 2

.= dom ((Carrier J) +* (product_basis_selector (J,f))) by FUNCT_4:def 1 ;

then consider h being Function such that

A117: ( h = x & dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) ) and

A118: for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds

h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by CARD_3:def 5;

for A being set st A in X holds

h in A

end;A92: I = I \/ (rng f) by XBOOLE_1:12

.= (dom (Carrier J)) \/ (rng f) by PARTFUN1:def 2

.= (dom (Carrier J)) \/ (dom (product_basis_selector (J,f))) by PARTFUN1:def 2

.= dom ((Carrier J) +* (product_basis_selector (J,f))) by FUNCT_4:def 1 ;

hereby :: thesis: ( x in product ((Carrier J) +* (product_basis_selector (J,f))) implies x in meet X )

assume
x in product ((Carrier J) +* (product_basis_selector (J,f)))
; :: thesis: x in meet Xassume A93:
x in meet X
; :: thesis: x in product ((Carrier J) +* (product_basis_selector (J,f)))

consider A0 being object such that

A94: A0 in X by A27, XBOOLE_0:def 1;

reconsider A0 = A0 as set by TARSKI:1;

consider i0 being Element of I such that

A95: ( f . A0 = i0 & A0 = meet (g " {i0}) & g " {i0} <> {} ) by A11, A94;

A0 <> {} by A3, A81, A94, SETFAM_1:4;

then consider Z0 being Subset-Family of (J . (In ((f . A0),I))) such that

Z0 = { ((proj (J,(In ((f . A0),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A0)} } and

( Z0 is open & Z0 is finite & not Z0 is empty ) and

A96: A0 = product ((Carrier J) +* ((f . A0),(meet Z0))) by A31, A94, A95;

x in A0 by A93, A94, SETFAM_1:def 1;

then consider h being Function such that

A97: ( x = h & dom h = dom ((Carrier J) +* ((f . A0),(meet Z0))) ) and

A98: for y being object st y in dom ((Carrier J) +* ((f . A0),(meet Z0))) holds

h . y in ((Carrier J) +* ((f . A0),(meet Z0))) . y by A96, CARD_3:def 5;

A99: dom h = I by A97, PARTFUN1:def 2;

A100: dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) by A92, A97, PARTFUN1:def 2;

for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds

h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

end;consider A0 being object such that

A94: A0 in X by A27, XBOOLE_0:def 1;

reconsider A0 = A0 as set by TARSKI:1;

consider i0 being Element of I such that

A95: ( f . A0 = i0 & A0 = meet (g " {i0}) & g " {i0} <> {} ) by A11, A94;

A0 <> {} by A3, A81, A94, SETFAM_1:4;

then consider Z0 being Subset-Family of (J . (In ((f . A0),I))) such that

Z0 = { ((proj (J,(In ((f . A0),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A0)} } and

( Z0 is open & Z0 is finite & not Z0 is empty ) and

A96: A0 = product ((Carrier J) +* ((f . A0),(meet Z0))) by A31, A94, A95;

x in A0 by A93, A94, SETFAM_1:def 1;

then consider h being Function such that

A97: ( x = h & dom h = dom ((Carrier J) +* ((f . A0),(meet Z0))) ) and

A98: for y being object st y in dom ((Carrier J) +* ((f . A0),(meet Z0))) holds

h . y in ((Carrier J) +* ((f . A0),(meet Z0))) . y by A96, CARD_3:def 5;

A99: dom h = I by A97, PARTFUN1:def 2;

A100: dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) by A92, A97, PARTFUN1:def 2;

for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds

h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

proof

hence
x in product ((Carrier J) +* (product_basis_selector (J,f)))
by A97, A100, CARD_3:def 5; :: thesis: verum
let y be object ; :: thesis: ( y in dom ((Carrier J) +* (product_basis_selector (J,f))) implies h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y )

assume y in dom ((Carrier J) +* (product_basis_selector (J,f))) ; :: thesis: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

then reconsider i = y as Element of I by A92;

i in dom h by A99;

then A101: i in dom (Carrier J) by A97, FUNCT_7:30;

end;assume y in dom ((Carrier J) +* (product_basis_selector (J,f))) ; :: thesis: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

then reconsider i = y as Element of I by A92;

i in dom h by A99;

then A101: i in dom (Carrier J) by A97, FUNCT_7:30;

per cases
( y in rng f or not y in rng f )
;

end;

suppose A102:
y in rng f
; :: thesis: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

then
y in dom (product_basis_selector (J,f))
by PARTFUN1:def 2;

then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i by FUNCT_4:13;

then A103: ((Carrier J) +* (product_basis_selector (J,f))) . y = (proj (J,i)) .: ((f ") . i) by A102, Th54;

consider A being object such that

A104: ( A in X & f . A = i ) by A102, FUNCT_2:11;

reconsider A = A as set by TARSKI:1;

consider j being Element of I such that

A105: ( f . A = j & A = meet (g " {j}) & g " {j} <> {} ) by A11, A104;

A <> {} by A3, A81, A104, SETFAM_1:4;

then consider Z being Subset-Family of (J . (In ((f . A),I))) such that

Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and

( Z is open & Z is finite & not Z is empty ) and

A106: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A104, A105;

reconsider Z = Z as Subset-Family of (J . i) by A104;

a107: h in A by A93, A97, A104, SETFAM_1:def 1;

dom ((Carrier J) +* ((f . A),(meet Z))) = I by PARTFUN1:def 2;

then h . i in ((Carrier J) +* ((f . A),(meet Z))) . i by a107, A106, CARD_3:9;

then A108: h . i in meet Z by A104, A101, FUNCT_7:31;

ex z being object st

( z in dom (proj (J,i)) & z in meet (g " {i}) & (proj (J,i)) . z = h . i )

hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A103, A105, A12, A104, FUNCT_1:34; :: thesis: verum

end;then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i by FUNCT_4:13;

then A103: ((Carrier J) +* (product_basis_selector (J,f))) . y = (proj (J,i)) .: ((f ") . i) by A102, Th54;

consider A being object such that

A104: ( A in X & f . A = i ) by A102, FUNCT_2:11;

reconsider A = A as set by TARSKI:1;

consider j being Element of I such that

A105: ( f . A = j & A = meet (g " {j}) & g " {j} <> {} ) by A11, A104;

A <> {} by A3, A81, A104, SETFAM_1:4;

then consider Z being Subset-Family of (J . (In ((f . A),I))) such that

Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and

( Z is open & Z is finite & not Z is empty ) and

A106: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A104, A105;

reconsider Z = Z as Subset-Family of (J . i) by A104;

a107: h in A by A93, A97, A104, SETFAM_1:def 1;

dom ((Carrier J) +* ((f . A),(meet Z))) = I by PARTFUN1:def 2;

then h . i in ((Carrier J) +* ((f . A),(meet Z))) . i by a107, A106, CARD_3:9;

then A108: h . i in meet Z by A104, A101, FUNCT_7:31;

ex z being object st

( z in dom (proj (J,i)) & z in meet (g " {i}) & (proj (J,i)) . z = h . i )

proof

then
h . i in (proj (J,i)) .: (meet (g " {i}))
by FUNCT_1:def 6;
set z0 = the Element of product (Carrier J);

set z = the Element of product (Carrier J) +* (i,(h . i));

take the Element of product (Carrier J) +* (i,(h . i)) ; :: thesis: ( the Element of product (Carrier J) +* (i,(h . i)) in dom (proj (J,i)) & the Element of product (Carrier J) +* (i,(h . i)) in meet (g " {i}) & (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i )

meet Z c= the carrier of (J . i) ;

then meet Z c= [#] (J . i) by STRUCT_0:def 3;

then A109: meet Z c= (Carrier J) . i by PENCIL_3:7;

A110: the Element of product (Carrier J) +* (i,(h . i)) in product ((Carrier J) +* (i,(meet Z))) by A101, A108, Th37;

product ((Carrier J) +* (i,(meet Z))) c= product (Carrier J) by A101, A109, Th39;

then the Element of product (Carrier J) +* (i,(h . i)) in product (Carrier J) by A110;

then A111: the Element of product (Carrier J) +* (i,(h . i)) in dom (proj ((Carrier J),i)) by CARD_3:def 16;

hence ( the Element of product (Carrier J) +* (i,(h . i)) in dom (proj (J,i)) & the Element of product (Carrier J) +* (i,(h . i)) in meet (g " {i}) ) by A104, A105, A106, A101, A108, Th37, WAYBEL18:def 4; :: thesis: (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i

A112: i in dom the Element of product (Carrier J) by A101, CARD_3:9;

thus (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = (proj ((Carrier J),i)) . ( the Element of product (Carrier J) +* (i,(h . i))) by WAYBEL18:def 4

.= ( the Element of product (Carrier J) +* (i,(h . i))) . i by A111, CARD_3:def 16

.= h . i by A112, FUNCT_7:31 ; :: thesis: verum

end;set z = the Element of product (Carrier J) +* (i,(h . i));

take the Element of product (Carrier J) +* (i,(h . i)) ; :: thesis: ( the Element of product (Carrier J) +* (i,(h . i)) in dom (proj (J,i)) & the Element of product (Carrier J) +* (i,(h . i)) in meet (g " {i}) & (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i )

meet Z c= the carrier of (J . i) ;

then meet Z c= [#] (J . i) by STRUCT_0:def 3;

then A109: meet Z c= (Carrier J) . i by PENCIL_3:7;

A110: the Element of product (Carrier J) +* (i,(h . i)) in product ((Carrier J) +* (i,(meet Z))) by A101, A108, Th37;

product ((Carrier J) +* (i,(meet Z))) c= product (Carrier J) by A101, A109, Th39;

then the Element of product (Carrier J) +* (i,(h . i)) in product (Carrier J) by A110;

then A111: the Element of product (Carrier J) +* (i,(h . i)) in dom (proj ((Carrier J),i)) by CARD_3:def 16;

hence ( the Element of product (Carrier J) +* (i,(h . i)) in dom (proj (J,i)) & the Element of product (Carrier J) +* (i,(h . i)) in meet (g " {i}) ) by A104, A105, A106, A101, A108, Th37, WAYBEL18:def 4; :: thesis: (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i

A112: i in dom the Element of product (Carrier J) by A101, CARD_3:9;

thus (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = (proj ((Carrier J),i)) . ( the Element of product (Carrier J) +* (i,(h . i))) by WAYBEL18:def 4

.= ( the Element of product (Carrier J) +* (i,(h . i))) . i by A111, CARD_3:def 16

.= h . i by A112, FUNCT_7:31 ; :: thesis: verum

hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A103, A105, A12, A104, FUNCT_1:34; :: thesis: verum

suppose
not y in rng f
; :: thesis: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

then
not y in dom (product_basis_selector (J,f))
;

then A114: ((Carrier J) +* (product_basis_selector (J,f))) . y = (Carrier J) . y by FUNCT_4:11;

reconsider Z0 = Z0 as Subset-Family of (J . i0) by A95;

meet Z0 c= the carrier of (J . i0) ;

then meet Z0 c= [#] (J . i0) by STRUCT_0:def 3;

then A115: meet Z0 c= (Carrier J) . i0 by PENCIL_3:7;

i0 in I ;

then i0 in dom (Carrier J) by PARTFUN1:def 2;

then A116: product ((Carrier J) +* (i0,(meet Z0))) c= product (Carrier J) by A115, Th39;

h in product ((Carrier J) +* (i0,(meet Z0))) by A95, A97, A98, CARD_3:9;

hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A114, A101, A116, CARD_3:9; :: thesis: verum

end;then A114: ((Carrier J) +* (product_basis_selector (J,f))) . y = (Carrier J) . y by FUNCT_4:11;

reconsider Z0 = Z0 as Subset-Family of (J . i0) by A95;

meet Z0 c= the carrier of (J . i0) ;

then meet Z0 c= [#] (J . i0) by STRUCT_0:def 3;

then A115: meet Z0 c= (Carrier J) . i0 by PENCIL_3:7;

i0 in I ;

then i0 in dom (Carrier J) by PARTFUN1:def 2;

then A116: product ((Carrier J) +* (i0,(meet Z0))) c= product (Carrier J) by A115, Th39;

h in product ((Carrier J) +* (i0,(meet Z0))) by A95, A97, A98, CARD_3:9;

hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A114, A101, A116, CARD_3:9; :: thesis: verum

then consider h being Function such that

A117: ( h = x & dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) ) and

A118: for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds

h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by CARD_3:def 5;

for A being set st A in X holds

h in A

proof

hence
x in meet X
by A27, A117, SETFAM_1:def 1; :: thesis: verum
let A be set ; :: thesis: ( A in X implies h in A )

assume A119: A in X ; :: thesis: h in A

then consider i being Element of I such that

A120: ( f . A = i & A = meet (g " {i}) & g " {i} <> {} ) by A11;

A121: (f ") . i = A by A12, A119, A120, FUNCT_1:34;

A <> {} by A3, A81, A119, SETFAM_1:4;

then consider Z being Subset-Family of (J . (In ((f . A),I))) such that

A122: Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and

( Z is open & Z is finite & not Z is empty ) and

A124: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A119, A120;

A125: dom h = dom ((Carrier J) +* ((f . A),(meet Z))) by A92, A117, PARTFUN1:def 2;

for y being object st y in dom ((Carrier J) +* ((f . A),(meet Z))) holds

h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

end;assume A119: A in X ; :: thesis: h in A

then consider i being Element of I such that

A120: ( f . A = i & A = meet (g " {i}) & g " {i} <> {} ) by A11;

A121: (f ") . i = A by A12, A119, A120, FUNCT_1:34;

A <> {} by A3, A81, A119, SETFAM_1:4;

then consider Z being Subset-Family of (J . (In ((f . A),I))) such that

A122: Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and

( Z is open & Z is finite & not Z is empty ) and

A124: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A119, A120;

A125: dom h = dom ((Carrier J) +* ((f . A),(meet Z))) by A92, A117, PARTFUN1:def 2;

for y being object st y in dom ((Carrier J) +* ((f . A),(meet Z))) holds

h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

proof

hence
h in A
by A124, A125, CARD_3:9; :: thesis: verum
let y be object ; :: thesis: ( y in dom ((Carrier J) +* ((f . A),(meet Z))) implies h . y in ((Carrier J) +* ((f . A),(meet Z))) . y )

assume A126: y in dom ((Carrier J) +* ((f . A),(meet Z))) ; :: thesis: h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

end;assume A126: y in dom ((Carrier J) +* ((f . A),(meet Z))) ; :: thesis: h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

per cases
( y <> i or y = i )
;

end;

suppose
y <> i
; :: thesis: h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

then A127:
((Carrier J) +* ((f . A),(meet Z))) . y = (Carrier J) . y
by A120, FUNCT_7:32;

A128: y in dom (Carrier J) by A126, FUNCT_7:30;

A129: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A92, A118, A126;

end;A128: y in dom (Carrier J) by A126, FUNCT_7:30;

A129: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A92, A118, A126;

per cases
( y in rng f or not y in rng f )
;

end;

suppose A130:
y in rng f
; :: thesis: h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

then reconsider i0 = y as Element of I ;

y in dom (product_basis_selector (J,f)) by A130, PARTFUN1:def 2;

then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i0 by FUNCT_4:13

.= (proj (J,i0)) .: ((f ") . i0) by A130, Th54 ;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj (J,i0)) by RELAT_1:111;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj ((Carrier J),i0)) by WAYBEL18:def 4;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= (Carrier J) . i0 by A128, YELLOW17:3;

hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A127, A129; :: thesis: verum

end;y in dom (product_basis_selector (J,f)) by A130, PARTFUN1:def 2;

then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i0 by FUNCT_4:13

.= (proj (J,i0)) .: ((f ") . i0) by A130, Th54 ;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj (J,i0)) by RELAT_1:111;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj ((Carrier J),i0)) by WAYBEL18:def 4;

then ((Carrier J) +* (product_basis_selector (J,f))) . y c= (Carrier J) . i0 by A128, YELLOW17:3;

hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A127, A129; :: thesis: verum

suppose A131:
y = i
; :: thesis: h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

i in I
;

then a132: i in dom (Carrier J) by PARTFUN1:def 2;

A133: i in rng f by A12, A119, A120, FUNCT_1:def 3;

then i in dom (product_basis_selector (J,f)) by PARTFUN1:def 2;

then A134: ((Carrier J) +* (product_basis_selector (J,f))) . i = (product_basis_selector (J,f)) . i by FUNCT_4:13

.= (proj (J,i)) .: (meet (g " {i})) by A120, A121, A133, Th54 ;

reconsider G = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;

h . i in (proj (J,i)) .: (meet (g " {i})) by A92, A118, A134;

then h . i in meet { ((proj (J,i)) .: B) where B is Subset of (product (Carrier J)) : B in G } by Th3, TARSKI:def 3;

hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A131, a132, FUNCT_7:31, A120, A122; :: thesis: verum

end;then a132: i in dom (Carrier J) by PARTFUN1:def 2;

A133: i in rng f by A12, A119, A120, FUNCT_1:def 3;

then i in dom (product_basis_selector (J,f)) by PARTFUN1:def 2;

then A134: ((Carrier J) +* (product_basis_selector (J,f))) . i = (product_basis_selector (J,f)) . i by FUNCT_4:13

.= (proj (J,i)) .: (meet (g " {i})) by A120, A121, A133, Th54 ;

reconsider G = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;

h . i in (proj (J,i)) .: (meet (g " {i})) by A92, A118, A134;

then h . i in meet { ((proj (J,i)) .: B) where B is Subset of (product (Carrier J)) : B in G } by Th3, TARSKI:def 3;

hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A131, a132, FUNCT_7:31, A120, A122; :: thesis: verum

suppose A136:
Y is empty
; :: thesis: ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

reconsider f = the empty Function as I -valued one-to-one Function by XBOOLE_1:2, RELAT_1:38, RELAT_1:def 19;

take Y ; :: thesis: ex f being I -valued one-to-one Function st

( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

take f ; :: thesis: ( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

thus ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A2; :: thesis: ( dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

thus dom f = Y by A136; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,f)))

product_basis_selector (J,f) is empty ;

hence P = product ((Carrier J) +* (product_basis_selector (J,f))) by A2, A136, SETFAM_1:def 9; :: thesis: verum

end;take Y ; :: thesis: ex f being I -valued one-to-one Function st

( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

take f ; :: thesis: ( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

thus ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A2; :: thesis: ( dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

thus dom f = Y by A136; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,f)))

product_basis_selector (J,f) is empty ;

hence P = product ((Carrier J) +* (product_basis_selector (J,f))) by A2, A136, SETFAM_1:def 9; :: thesis: verum

suppose
( not Y is empty & meet Y = {} )
; :: thesis: ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

then A138:
P = {}
by A2, SETFAM_1:def 9;

set i = the Element of I;

set V = the empty Subset of (J . the Element of I);

a139: dom (Carrier J) = I by PARTFUN1:def 2;

then A140: product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) = {} by Th36;

then product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) in product_prebasis J by Th56;

then reconsider A = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) as Subset of (product (Carrier J)) ;

set X = {A};

set f = A .--> the Element of I;

take {A} ; :: thesis: ex f being I -valued one-to-one Function st

( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom f = {A} & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

take A .--> the Element of I ; :: thesis: ( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

thus ( {A} c= product_prebasis J & {A} is finite ) by A140, Th56, ZFMISC_1:31; :: thesis: ( P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

{} in {A} by A140, TARSKI:def 1;

then meet {A} = {} by SETFAM_1:4;

hence P = Intersect {A} by A138, SETFAM_1:def 9; :: thesis: ( dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

thus dom (A .--> the Element of I) = dom ({A} --> the Element of I) by FUNCOP_1:def 9

.= {A} ; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))

set F = (Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)));

ex j being object st

( j in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) & ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . j = {} )

hence P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by A138, CARD_3:26; :: thesis: verum

end;set i = the Element of I;

set V = the empty Subset of (J . the Element of I);

a139: dom (Carrier J) = I by PARTFUN1:def 2;

then A140: product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) = {} by Th36;

then product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) in product_prebasis J by Th56;

then reconsider A = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) as Subset of (product (Carrier J)) ;

set X = {A};

set f = A .--> the Element of I;

take {A} ; :: thesis: ex f being I -valued one-to-one Function st

( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom f = {A} & P = product ((Carrier J) +* (product_basis_selector (J,f))) )

take A .--> the Element of I ; :: thesis: ( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

thus ( {A} c= product_prebasis J & {A} is finite ) by A140, Th56, ZFMISC_1:31; :: thesis: ( P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

{} in {A} by A140, TARSKI:def 1;

then meet {A} = {} by SETFAM_1:4;

hence P = Intersect {A} by A138, SETFAM_1:def 9; :: thesis: ( dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )

thus dom (A .--> the Element of I) = dom ({A} --> the Element of I) by FUNCOP_1:def 9

.= {A} ; :: thesis: P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))

set F = (Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)));

ex j being object st

( j in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) & ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . j = {} )

proof

then
{} in rng ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))
by FUNCT_1:def 3;
take
the Element of I
; :: thesis: ( the Element of I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) & ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {} )

the Element of I in (dom (Carrier J)) \/ (dom (product_basis_selector (J,(A .--> the Element of I)))) by a139, XBOOLE_1:7, TARSKI:def 3;

hence the Element of I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_4:def 1; :: thesis: ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {}

the Element of I in { the Element of I} by TARSKI:def 1;

then the Element of I in rng ({A} --> the Element of I) by FUNCOP_1:8;

then A142: the Element of I in rng (A .--> the Element of I) by FUNCOP_1:def 9;

then the Element of I in dom (product_basis_selector (J,(A .--> the Element of I))) by PARTFUN1:def 2;

hence ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = (product_basis_selector (J,(A .--> the Element of I))) . the Element of I by FUNCT_4:13

.= (proj (J, the Element of I)) .: (((A .--> the Element of I) ") . the Element of I) by A142, Th54

.= (proj (J, the Element of I)) .: (( the Element of I .--> A) . the Element of I) by NECKLACE:9

.= (proj (J, the Element of I)) .: A by FUNCOP_1:72

.= {} by A140 ;

:: thesis: verum

end;the Element of I in (dom (Carrier J)) \/ (dom (product_basis_selector (J,(A .--> the Element of I)))) by a139, XBOOLE_1:7, TARSKI:def 3;

hence the Element of I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_4:def 1; :: thesis: ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {}

the Element of I in { the Element of I} by TARSKI:def 1;

then the Element of I in rng ({A} --> the Element of I) by FUNCOP_1:8;

then A142: the Element of I in rng (A .--> the Element of I) by FUNCOP_1:def 9;

then the Element of I in dom (product_basis_selector (J,(A .--> the Element of I))) by PARTFUN1:def 2;

hence ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = (product_basis_selector (J,(A .--> the Element of I))) . the Element of I by FUNCT_4:13

.= (proj (J, the Element of I)) .: (((A .--> the Element of I) ") . the Element of I) by A142, Th54

.= (proj (J, the Element of I)) .: (( the Element of I .--> A) . the Element of I) by NECKLACE:9

.= (proj (J, the Element of I)) .: A by FUNCOP_1:72

.= {} by A140 ;

:: thesis: verum

hence P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by A138, CARD_3:26; :: thesis: verum