let n be Nat; :: thesis: ( n <> 0 implies for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds

PP is quasi_prebasis )

assume A1: n <> 0 ; :: thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds

PP is quasi_prebasis

set E = Euclid n;

set T = TopSpaceMetr (Euclid n);

let PP be Subset-Family of (TopSpaceMetr (Euclid n)); :: thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is quasi_prebasis )

set J = (Seg n) --> R^1;

set C = Carrier ((Seg n) --> R^1);

set S = Seg n;

reconsider S = Seg n as non empty finite set by A1;

assume A2: PP = product_prebasis ((Seg n) --> R^1) ; :: thesis: PP is quasi_prebasis

A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;

A4: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def 2;

A5: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25;

defpred S_{1}[ set , object ] means ex e being Point of (Euclid n) st

( e = $1 & $2 = OpenHypercubes e );

A6: for i being Element of (TopSpaceMetr (Euclid n)) ex j being object st S_{1}[i,j]

A7: for x being Point of (TopSpaceMetr (Euclid n)) holds S_{1}[x,NS . x]
from PBOOLE:sch 6(A6);

take B = Union NS; :: according to CANTOR_1:def 4 :: thesis: B c= FinMeetCl PP

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in FinMeetCl PP )

reconsider bb = b as set by TARSKI:1;

assume b in B ; :: thesis: b in FinMeetCl PP

then consider Z being set such that

A8: b in Z and

A9: Z in rng NS by TARSKI:def 4;

consider x being object such that

A10: x in dom NS and

A11: NS . x = Z by A9, FUNCT_1:def 3;

reconsider x = x as Point of (Euclid n) by A10;

A12: dom x = Seg n by FINSEQ_1:89;

S_{1}[x,NS . x]
by A7;

then consider m being non zero Element of NAT such that

A13: b = OpenHypercube (x,(1 / m)) by A8, A11;

deffunc H_{2}( object ) -> set = product ((Carrier ((Seg n) --> R^1)) +* ($1,(R^1 ].((x . $1) - (1 / m)),((x . $1) + (1 / m)).[)));

defpred S_{2}[ set ] means verum;

set Y = { H_{2}(q) where q is Element of S : S_{2}[q] } ;

A14: { H_{2}(q) where q is Element of S : S_{2}[q] } is finite
from PRE_CIRC:sch 1();

{ H_{2}(q) where q is Element of S : S_{2}[q] } c= bool the carrier of (TopSpaceMetr (Euclid n))
_{2}(q) where q is Element of S : S_{2}[q] } as Subset-Family of (TopSpaceMetr (Euclid n)) ;

A25: Y c= PP

A28: N in S by XBOOLE_0:def 1;

A29: H_{2}(N) in Y
by A28;

then A30: Intersect Y = meet Y by SETFAM_1:def 9;

A31: dom (Intervals (x,(1 / m))) = dom x by Def3;

PP is quasi_prebasis )

assume A1: n <> 0 ; :: thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds

PP is quasi_prebasis

set E = Euclid n;

set T = TopSpaceMetr (Euclid n);

let PP be Subset-Family of (TopSpaceMetr (Euclid n)); :: thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is quasi_prebasis )

set J = (Seg n) --> R^1;

set C = Carrier ((Seg n) --> R^1);

set S = Seg n;

reconsider S = Seg n as non empty finite set by A1;

assume A2: PP = product_prebasis ((Seg n) --> R^1) ; :: thesis: PP is quasi_prebasis

A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;

A4: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def 2;

A5: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25;

defpred S

( e = $1 & $2 = OpenHypercubes e );

A6: for i being Element of (TopSpaceMetr (Euclid n)) ex j being object st S

proof

consider NS being ManySortedSet of (TopSpaceMetr (Euclid n)) such that
let i be Element of (TopSpaceMetr (Euclid n)); :: thesis: ex j being object st S_{1}[i,j]

reconsider j = i as Point of (Euclid n) ;

take OpenHypercubes j ; :: thesis: S_{1}[i, OpenHypercubes j]

take j ; :: thesis: ( j = i & OpenHypercubes j = OpenHypercubes j )

thus ( j = i & OpenHypercubes j = OpenHypercubes j ) ; :: thesis: verum

end;reconsider j = i as Point of (Euclid n) ;

take OpenHypercubes j ; :: thesis: S

take j ; :: thesis: ( j = i & OpenHypercubes j = OpenHypercubes j )

thus ( j = i & OpenHypercubes j = OpenHypercubes j ) ; :: thesis: verum

A7: for x being Point of (TopSpaceMetr (Euclid n)) holds S

now :: thesis: for x being Point of (TopSpaceMetr (Euclid n)) holds NS . x is Basis of x

then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def 3;let x be Point of (TopSpaceMetr (Euclid n)); :: thesis: NS . x is Basis of x

reconsider y = x as Point of (Euclid n) ;

S_{1}[y,NS . y]
by A7;

hence NS . x is Basis of x ; :: thesis: verum

end;reconsider y = x as Point of (Euclid n) ;

S

hence NS . x is Basis of x ; :: thesis: verum

take B = Union NS; :: according to CANTOR_1:def 4 :: thesis: B c= FinMeetCl PP

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in FinMeetCl PP )

reconsider bb = b as set by TARSKI:1;

assume b in B ; :: thesis: b in FinMeetCl PP

then consider Z being set such that

A8: b in Z and

A9: Z in rng NS by TARSKI:def 4;

consider x being object such that

A10: x in dom NS and

A11: NS . x = Z by A9, FUNCT_1:def 3;

reconsider x = x as Point of (Euclid n) by A10;

A12: dom x = Seg n by FINSEQ_1:89;

S

then consider m being non zero Element of NAT such that

A13: b = OpenHypercube (x,(1 / m)) by A8, A11;

deffunc H

defpred S

set Y = { H

A14: { H

{ H

proof

then reconsider Y = { H
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { H_{2}(q) where q is Element of S : S_{2}[q] } or s in bool the carrier of (TopSpaceMetr (Euclid n)) )

assume s in { H_{2}(q) where q is Element of S : S_{2}[q] }
; :: thesis: s in bool the carrier of (TopSpaceMetr (Euclid n))

then consider q being Element of S such that

A15: s = H_{2}(q)
;

H_{2}(q) c= the carrier of (TopSpaceMetr (Euclid n))

end;assume s in { H

then consider q being Element of S such that

A15: s = H

H

proof

hence
s in bool the carrier of (TopSpaceMetr (Euclid n))
by A15, ZFMISC_1:def 1; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H_{2}(q) or z in the carrier of (TopSpaceMetr (Euclid n)) )

set f = (Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[));

assume z in H_{2}(q)
; :: thesis: z in the carrier of (TopSpaceMetr (Euclid n))

then consider g being Function such that

A16: z = g and

A17: dom g = dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) and

A18: for d being object st d in dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) holds

g . d in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . d by CARD_3:def 5;

A19: dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

then reconsider g = g as FinSequence by A4, A17, FINSEQ_1:def 2;

rng g c= REAL

then A24: g is Element of REAL * by FINSEQ_1:def 11;

n in NAT by ORDINAL1:def 12;

then len g = n by A4, A17, A19, FINSEQ_1:def 3;

hence z in the carrier of (TopSpaceMetr (Euclid n)) by A16, A24; :: thesis: verum

end;set f = (Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[));

assume z in H

then consider g being Function such that

A16: z = g and

A17: dom g = dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) and

A18: for d being object st d in dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) holds

g . d in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . d by CARD_3:def 5;

A19: dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

then reconsider g = g as FinSequence by A4, A17, FINSEQ_1:def 2;

rng g c= REAL

proof

then
g is FinSequence of REAL
by FINSEQ_1:def 4;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng g or b in REAL )

assume b in rng g ; :: thesis: b in REAL

then consider a being object such that

A20: a in dom g and

A21: g . a = b by FUNCT_1:def 3;

A22: g . a in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a by A17, A18, A20;

end;assume b in rng g ; :: thesis: b in REAL

then consider a being object such that

A20: a in dom g and

A21: g . a = b by FUNCT_1:def 3;

A22: g . a in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a by A17, A18, A20;

per cases
( a = q or a <> q )
;

end;

suppose
a = q
; :: thesis: b in REAL

then
((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[
by A17, A19, A20, FUNCT_7:31;

hence b in REAL by A21, A22; :: thesis: verum

end;hence b in REAL by A21, A22; :: thesis: verum

suppose
a <> q
; :: thesis: b in REAL

then A23:
((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = (Carrier ((Seg n) --> R^1)) . a
by FUNCT_7:32;

ex R being 1-sorted st

( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A20, A17, A19, PRALG_1:def 15;

hence b in REAL by A21, A22, A23, A20, A17, A19, FUNCOP_1:7; :: thesis: verum

end;ex R being 1-sorted st

( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A20, A17, A19, PRALG_1:def 15;

hence b in REAL by A21, A22, A23, A20, A17, A19, FUNCOP_1:7; :: thesis: verum

then A24: g is Element of REAL * by FINSEQ_1:def 11;

n in NAT by ORDINAL1:def 12;

then len g = n by A4, A17, A19, FINSEQ_1:def 3;

hence z in the carrier of (TopSpaceMetr (Euclid n)) by A16, A24; :: thesis: verum

A25: Y c= PP

proof

consider N being object such that
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Y or z in PP )

assume A26: z in Y ; :: thesis: z in PP

then consider i being Element of S such that

A27: z = H_{2}(i)
;

((Seg n) --> R^1) . i = R^1 ;

hence z in PP by A2, A5, A26, A3, A27, WAYBEL18:def 2; :: thesis: verum

end;assume A26: z in Y ; :: thesis: z in PP

then consider i being Element of S such that

A27: z = H

((Seg n) --> R^1) . i = R^1 ;

hence z in PP by A2, A5, A26, A3, A27, WAYBEL18:def 2; :: thesis: verum

A28: N in S by XBOOLE_0:def 1;

A29: H

then A30: Intersect Y = meet Y by SETFAM_1:def 9;

A31: dom (Intervals (x,(1 / m))) = dom x by Def3;

A32: now :: thesis: for i being Element of S holds product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))

bb = Intersect Y
let i be Element of S; :: thesis: product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))

set f = (Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[));

thus product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) :: thesis: verum

end;set f = (Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[));

thus product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) :: thesis: verum

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in product (Intervals (x,(1 / m))) or d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) )

assume d in product (Intervals (x,(1 / m))) ; :: thesis: d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))

then consider d1 being Function such that

A33: d = d1 and

A34: dom d1 = dom (Intervals (x,(1 / m))) and

A35: for a being object st a in dom (Intervals (x,(1 / m))) holds

d1 . a in (Intervals (x,(1 / m))) . a by CARD_3:def 5;

A36: dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

end;assume d in product (Intervals (x,(1 / m))) ; :: thesis: d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))

then consider d1 being Function such that

A33: d = d1 and

A34: dom d1 = dom (Intervals (x,(1 / m))) and

A35: for a being object st a in dom (Intervals (x,(1 / m))) holds

d1 . a in (Intervals (x,(1 / m))) . a by CARD_3:def 5;

A36: dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

now :: thesis: for k being object st k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) holds

d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k

hence
d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
by A33, A4, A34, A31, A12, A36, CARD_3:9; :: thesis: verumd1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k

let k be object ; :: thesis: ( k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) implies d1 . b_{1} in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b_{1} )

assume A37: k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ; :: thesis: d1 . b_{1} in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b_{1}

then A38: (Intervals (x,(1 / m))) . k = ].((x . k) - (1 / m)),((x . k) + (1 / m)).[ by A36, A12, Def3;

A39: d1 . k in (Intervals (x,(1 / m))) . k by A35, A31, A12, A36, A37;

end;assume A37: k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ; :: thesis: d1 . b

then A38: (Intervals (x,(1 / m))) . k = ].((x . k) - (1 / m)),((x . k) + (1 / m)).[ by A36, A12, Def3;

A39: d1 . k in (Intervals (x,(1 / m))) . k by A35, A31, A12, A36, A37;

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

end;

suppose
k = i
; :: thesis: d1 . b_{1} in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b_{1}

hence
d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k
by A38, A39, A37, A36, FUNCT_7:31; :: thesis: verum

end;suppose
k <> i
; :: thesis: d1 . b_{1} in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b_{1}

then A40:
((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k = (Carrier ((Seg n) --> R^1)) . k
by FUNCT_7:32;

A41: ex R being 1-sorted st

( R = ((Seg n) --> R^1) . k & (Carrier ((Seg n) --> R^1)) . k = the carrier of R ) by A37, A36, PRALG_1:def 15;

d1 . k in REAL by A38, A39;

hence d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A40, A41, A37, A36, FUNCOP_1:7; :: thesis: verum

end;A41: ex R being 1-sorted st

( R = ((Seg n) --> R^1) . k & (Carrier ((Seg n) --> R^1)) . k = the carrier of R ) by A37, A36, PRALG_1:def 15;

d1 . k in REAL by A38, A39;

hence d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A40, A41, A37, A36, FUNCOP_1:7; :: thesis: verum

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect Y or q in bb )

assume A42: q in Intersect Y ; :: thesis: q in bb

then reconsider q = q as Function ;

A43: dom q = Seg n by A42, FINSEQ_1:89;

end;

hence
b in FinMeetCl PP
by A25, A14, CANTOR_1:def 3; :: thesis: verumnow :: thesis: for M being set st M in Y holds

bb c= M

hence
bb c= Intersect Y
by A30, A29, SETFAM_1:5; :: according to XBOOLE_0:def 10 :: thesis: Intersect Y c= bbbb c= M

let M be set ; :: thesis: ( M in Y implies bb c= M )

assume M in Y ; :: thesis: bb c= M

then ex i being Element of S st M = H_{2}(i)
;

hence bb c= M by A13, A32; :: thesis: verum

end;assume M in Y ; :: thesis: bb c= M

then ex i being Element of S st M = H

hence bb c= M by A13, A32; :: thesis: verum

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect Y or q in bb )

assume A42: q in Intersect Y ; :: thesis: q in bb

then reconsider q = q as Function ;

A43: dom q = Seg n by A42, FINSEQ_1:89;

now :: thesis: for a being object st a in dom (Intervals (x,(1 / m))) holds

q . a in (Intervals (x,(1 / m))) . a

hence
q in bb
by A13, A43, A31, A12, CARD_3:9; :: thesis: verumq . a in (Intervals (x,(1 / m))) . a

let a be object ; :: thesis: ( a in dom (Intervals (x,(1 / m))) implies q . a in (Intervals (x,(1 / m))) . a )

assume A44: a in dom (Intervals (x,(1 / m))) ; :: thesis: q . a in (Intervals (x,(1 / m))) . a

A45: (Intervals (x,(1 / m))) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[ by A44, A31, Def3;

set f = (Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[));

H_{2}(a) in Y
by A44, A31, A12;

then A46: q in H_{2}(a)
by A42, SETFAM_1:43;

then A47: dom q = dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) by CARD_3:9;

then A48: q . a in ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) . a by A43, A44, A31, A12, A46, CARD_3:9;

dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

hence q . a in (Intervals (x,(1 / m))) . a by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:31; :: thesis: verum

end;assume A44: a in dom (Intervals (x,(1 / m))) ; :: thesis: q . a in (Intervals (x,(1 / m))) . a

A45: (Intervals (x,(1 / m))) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[ by A44, A31, Def3;

set f = (Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[));

H

then A46: q in H

then A47: dom q = dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) by CARD_3:9;

then A48: q . a in ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) . a by A43, A44, A31, A12, A46, CARD_3:9;

dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

hence q . a in (Intervals (x,(1 / m))) . a by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:31; :: thesis: verum