let a be Real; :: thesis: for A being closed-interval Subset of REAL st not - a in A holds
((AffineMap 1,a) ^ ) | A is continuous
let A be closed-interval Subset of REAL ; :: thesis: ( not - a in A implies ((AffineMap 1,a) ^ ) | A is continuous )
assume AA: not - a in A ; :: thesis: ((AffineMap 1,a) ^ ) | A is continuous
set g2 = AffineMap 1,a;
set i2 = (AffineMap 1,a) ^ ;
A3: dom (AffineMap 1,a) = [#] REAL by FUNCT_2:def 1;
(AffineMap 1,a) | (dom (AffineMap 1,a)) is continuous by RELAT_1:98;
then A2: (AffineMap 1,a) | A is continuous by A3, FCONT_1:17;
not 0 in rng ((AffineMap 1,a) | A)

proof

set h2 = (AffineMap 1,a) | A;
assume 0 in rng ((AffineMap 1,a) | A) ; :: thesis: contradiction
then consider x being set such that
C1: ( x in dom ((AffineMap 1,a) | A) & ((AffineMap 1,a) | A) . x = 0 ) by FUNCT_1:def 5;
reconsider d = x as Real by C1;
C4: dom ((AffineMap 1,a) | A) c= A by RELAT_1:87;
Af: d in A by C1, RELAT_1:86;
(AffineMap 1,a) . d = a + (1 * d) by JORDAN16:def 3;
then a + d = 0 by C1, Af, FUNCT_1:72;
hence contradiction by AA, C4, C1; :: thesis: verum

end;

then ((AffineMap 1,a) | A) " {0 } = {} by FUNCT_1:142;
hence ((AffineMap 1,a) ^ ) | A is continuous by A2, FCONT_1:24; :: thesis: verum