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

assume A1: <*p,q*> is_in_the_area_of f ; :: thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f )
dom <*p,q*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then ( 1 in dom <*p,q*> & <*p,q*> /. 1 = p & 2 in dom <*p,q*> & <*p,q*> /. 2 = q ) by FINSEQ_4:26, TARSKI:def 2;
then A2: ( W-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) & S-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) & W-bound (L~ f) <= q `1 & q `1 <= E-bound (L~ f) & S-bound (L~ f) <= q `2 & q `2 <= N-bound (L~ f) ) by A1, SPRECT_2:def 1;
thus <*p*> is_in_the_area_of f :: thesis: <*q*> is_in_the_area_of f

proof

let i be Element of 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:4, FINSEQ_1:55;
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 A2, FINSEQ_4:25; :: thesis: verum

end;

let i be Element of 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:4, FINSEQ_1:55;
then i = 1 by TARSKI:def 1;
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 A2, FINSEQ_4:25; :: thesis: verum

end;

assume A3: <*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 )
dom <*p*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then ( 1 in dom <*p*> & <*p*> /. 1 = p ) by FINSEQ_4:25, TARSKI:def 1;
then A4: ( W-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) & S-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) ) by A3, SPRECT_2:def 1;
assume A5: <*q*> is_in_the_area_of f ; :: thesis: <*p,q*> is_in_the_area_of f
dom <*q*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then ( 1 in dom <*q*> & <*q*> /. 1 = q ) by FINSEQ_4:25, TARSKI:def 1;
then A6: ( W-bound (L~ f) <= q `1 & q `1 <= E-bound (L~ f) & S-bound (L~ f) <= q `2 & q `2 <= N-bound (L~ f) ) by A5, SPRECT_2:def 1;
let i be Element of 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:4, FINSEQ_3:29;
then ( i = 1 or i = 2 ) by TARSKI:def 2;
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 A4, A6, FINSEQ_4:26; :: thesis: verum