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 )
set g2 = AffineMap 1,a;
set i2 = (AffineMap 1,a) ^ ;
assume A1: not - a in A ; :: thesis: ((AffineMap 1,a) ^ ) | A is continuous
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
A2: x in dom ((AffineMap 1,a) | A) and
A3: ((AffineMap 1,a) | A) . x = 0 by FUNCT_1:def 5;
reconsider d = x as Real by A2;
A4: (AffineMap 1,a) . d = a + (1 * d) by JORDAN16:def 3;
d in A by A2, RELAT_1:86;
then ( dom ((AffineMap 1,a) | A) c= A & a + d = 0 ) by A3, A4, FUNCT_1:72, RELAT_1:87;
hence contradiction by A1, A2; :: thesis: verum

end;

then A5: ((AffineMap 1,a) | A) " {0 } = {} by FUNCT_1:142;
( dom (AffineMap 1,a) = [#] REAL & (AffineMap 1,a) | (dom (AffineMap 1,a)) is continuous ) by FUNCT_2:def 1, RELAT_1:98;
then (AffineMap 1,a) | A is continuous by FCONT_1:17;
hence ((AffineMap 1,a) ^ ) | A is continuous by A5, FCONT_1:24; :: thesis: verum