let a, b, p, q, s be Real; ((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[) is Function of REAL,REAL
set g = ((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[);
set g1 = (AffineMap (a,b)) | ].-infty,s.[;
set g2 = (AffineMap (p,q)) | [.s,+infty.[;
D3:
( -infty < s & s < +infty )
by XXREAL_0:9, XXREAL_0:12, XREAL_0:def 1;
Dg: dom (((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) =
(dom ((AffineMap (a,b)) | ].-infty,s.[)) \/ (dom ((AffineMap (p,q)) | [.s,+infty.[))
by FUNCT_4:def 1
.=
].-infty,s.[ \/ (dom ((AffineMap (p,q)) | [.s,+infty.[))
by FUNCT_2:def 1
.=
].-infty,s.[ \/ [.s,+infty.[
by FUNCT_2:def 1
.=
REAL
by XXREAL_1:224, XXREAL_1:173, D3
;
for x being object st x in REAL holds
(((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) . x in REAL
proof
let x be
object ;
( x in REAL implies (((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) . x in REAL )
assume
x in REAL
;
(((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) . x in REAL
then reconsider x =
x as
Real ;
thus
(((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) . x in REAL
by XREAL_0:def 1;
verum
end;
hence
((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[) is Function of REAL,REAL
by FUNCT_2:3, Dg; verum