let f, g, h be FinSequence of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f & h is_in_the_area_of f implies g ^ h is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: h is_in_the_area_of f ; :: thesis: g ^ h is_in_the_area_of f
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( n in dom (g ^ h) implies ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) ) )
assume A3: n in dom (g ^ h) ; :: thesis: ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) )
per cases ( n in dom g or ex i being Nat st
( i in dom h & n = (len g) + i ) ) by A3, FINSEQ_1:25;
suppose A4: n in dom g ; :: thesis: ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) )
then (g ^ h) /. n = g /. n by FINSEQ_4:68;
hence ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) ) by A1, A4; :: thesis: verum
end;
suppose ex i being Nat st
( i in dom h & n = (len g) + i ) ; :: thesis: ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) )
then consider i being Nat such that
A5: i in dom h and
A6: n = (len g) + i ;
(g ^ h) /. n = h /. i by A5, A6, FINSEQ_4:69;
hence ( W-bound (L~ f) <= ((g ^ h) /. n) `1 & ((g ^ h) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((g ^ h) /. n) `2 & ((g ^ h) /. n) `2 <= N-bound (L~ f) ) by A2, A5; :: thesis: verum
end;
end;