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

proof

let x be object ; :: thesis: ( x in REAL implies (((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[)) . x in REAL )
assume x in REAL ; :: thesis: (((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; :: thesis: verum

end;

hence ((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[) is Function of REAL,REAL by FUNCT_2:3, Dg; :: thesis: verum