let a be Real; 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; ( not - a in A implies ((AffineMap (1,a)) ^) | A is continuous )
set g2 = AffineMap (1,a);
assume A1:
not - a in A
; ((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)
;
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;
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; verum