let a be Real; for A being non empty closed_interval Subset of REAL st not - a in A holds
((AffineMap (1,a)) ^) | A is continuous
let A be non empty 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
object such that A2:
x in dom ((AffineMap (1,a)) | A)
and A3:
((AffineMap (1,a)) | A) . x = 0
by FUNCT_1:def 3;
reconsider d =
x as
Element of
REAL by A2;
A4:
(AffineMap (1,a)) . d = a + (1 * d)
by FCONT_1:def 4;
d in A
by A2, RELAT_1:57;
then
(
dom ((AffineMap (1,a)) | A) c= A &
a + d = 0 )
by A3, A4, FUNCT_1:49, RELAT_1:58;
hence
contradiction
by A1, A2;
verum
end;
then A5:
((AffineMap (1,a)) | A) " {0} = {}
by FUNCT_1:72;
thus
((AffineMap (1,a)) ^) | A is continuous
by A5, FCONT_1:23; verum