let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( <*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 ) ) :: thesis: ( <*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 ; :: thesis: ( <*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 :: thesis: <*q*> is_in_the_area_of f

proof

let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not i in dom <*p*> or ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) )
assume i in dom <*p*> ; :: thesis: ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) )
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
hence ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) by A8, A5, A7, A6, FINSEQ_4:16; :: thesis: verum

end;

let i be Nat; :: according to SPRECT_2:def 1 :: thesis: ( 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*> ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: <*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; :: according to SPRECT_2:def 1 :: thesis: ( 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*> ; :: thesis: ( 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; :: thesis: verum