let a, b, c, p, q be Real; :: thesis: ( a < b & b < c implies ((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.]) = (AffineMap (p,q)) | [.a,c.] )
assume A1: ( a < b & b < c ) ; :: thesis: ((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.]) = (AffineMap (p,q)) | [.a,c.]
set f = AffineMap (p,q);
A2: dom (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) = (dom ((AffineMap (p,q)) | [.a,b.])) \/ (dom ((AffineMap (p,q)) | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom ((AffineMap (p,q)) | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.a,c.] by XXREAL_1:165, A1
.= dom ((AffineMap (p,q)) | [.a,c.]) by FUNCT_2:def 1 ;
for x being object st x in dom ((AffineMap (p,q)) | [.a,c.]) holds
((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x

proof

let x be object ; :: thesis: ( x in dom ((AffineMap (p,q)) | [.a,c.]) implies ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x )
assume A3: x in dom ((AffineMap (p,q)) | [.a,c.]) ; :: thesis: ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x
then reconsider x = x as Real ;
AA6: ( a <= x & x <= c ) by XXREAL_1:1, A3;

per cases ( b <= x or b > x ) ;

suppose b <= x ; :: thesis: ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x

then A8: x in [.b,c.] by AA6;
then A7: x in dom ((AffineMap (p,q)) | [.b,c.]) by FUNCT_2:def 1;
(((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x = ((AffineMap (p,q)) | [.b,c.]) . x by FUNCT_4:13, A7
.= (AffineMap (p,q)) . x by FUNCT_1:49, A8 ;
hence ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x by FUNCT_1:49, A3; :: thesis: verum

end;

suppose A5: b > x ; :: thesis: ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x

then A9: x in [.a,b.] by AA6;
not x in dom ((AffineMap (p,q)) | [.b,c.]) by XXREAL_1:1, A5;
then (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x = ((AffineMap (p,q)) | [.a,b.]) . x by FUNCT_4:11
.= (AffineMap (p,q)) . x by FUNCT_1:49, A9 ;
hence ((AffineMap (p,q)) | [.a,c.]) . x = (((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.])) . x by FUNCT_1:49, A3; :: thesis: verum

end;

end;

end;

hence ((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.]) = (AffineMap (p,q)) | [.a,c.] by A2, FUNCT_1:2; :: thesis: verum