let a, b, p, q, s be Real; :: thesis: ((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 by XREAL_0:def 1;
hence ((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[) is Function of REAL,REAL by FUNCT_2:3, Dg; :: thesis: verum