let f be FinSequence of (TOP-REAL 2); for p, q being Point of (TOP-REAL 2) holds
( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
let p, q be Point of (TOP-REAL 2); ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
thus
( <*p,q*> is_in_the_area_of f implies ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f implies <*p,q*> is_in_the_area_of f )proof
A1:
dom <*p,q*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then A2:
1
in dom <*p,q*>
by TARSKI:def 2;
assume A3:
<*p,q*> is_in_the_area_of f
;
( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f )
A4:
<*p,q*> /. 1
= p
by FINSEQ_4:17;
then A5:
p `1 <= E-bound (L~ f)
by A3, A2;
A6:
p `2 <= N-bound (L~ f)
by A3, A2, A4;
A7:
S-bound (L~ f) <= p `2
by A3, A2, A4;
A8:
W-bound (L~ f) <= p `1
by A3, A2, A4;
thus
<*p*> is_in_the_area_of f
<*q*> is_in_the_area_of f
let i be
Nat;
SPRECT_2:def 1 ( not i in dom <*q*> or ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) )
assume
i in dom <*q*>
;
( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) )
then
i in {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A9:
i = 1
by TARSKI:def 1;
A10:
<*p,q*> /. 2
= q
by FINSEQ_4:17;
A11:
2
in dom <*p,q*>
by A1, TARSKI:def 2;
then A12:
q `1 <= E-bound (L~ f)
by A3, A10;
A13:
q `2 <= N-bound (L~ f)
by A3, A11, A10;
A14:
S-bound (L~ f) <= q `2
by A3, A11, A10;
W-bound (L~ f) <= q `1
by A3, A11, A10;
hence
(
W-bound (L~ f) <= (<*q*> /. i) `1 &
(<*q*> /. i) `1 <= E-bound (L~ f) &
S-bound (L~ f) <= (<*q*> /. i) `2 &
(<*q*> /. i) `2 <= N-bound (L~ f) )
by A12, A14, A13, A9, FINSEQ_4:16;
verum
end;
A15:
<*p*> /. 1 = p
by FINSEQ_4:16;
dom <*q*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A16:
1 in dom <*q*>
by TARSKI:def 1;
dom <*p*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A17:
1 in dom <*p*>
by TARSKI:def 1;
assume A18:
<*p*> is_in_the_area_of f
; ( not <*q*> is_in_the_area_of f or <*p,q*> is_in_the_area_of f )
then A19:
p `1 <= E-bound (L~ f)
by A17, A15;
A20:
p `2 <= N-bound (L~ f)
by A18, A17, A15;
A21:
S-bound (L~ f) <= p `2
by A18, A17, A15;
A22:
<*q*> /. 1 = q
by FINSEQ_4:16;
assume A23:
<*q*> is_in_the_area_of f
; <*p,q*> is_in_the_area_of f
then A24:
W-bound (L~ f) <= q `1
by A16, A22;
A25:
q `1 <= E-bound (L~ f)
by A23, A16, A22;
let i be Nat; SPRECT_2:def 1 ( not i in dom <*p,q*> or ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) )
assume
i in dom <*p,q*>
; ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) )
then
i in {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then A26:
( i = 1 or i = 2 )
by TARSKI:def 2;
A27:
q `2 <= N-bound (L~ f)
by A23, A16, A22;
A28:
S-bound (L~ f) <= q `2
by A23, A16, A22;
W-bound (L~ f) <= p `1
by A18, A17, A15;
hence
( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) )
by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4:17; verum