let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, p, q being Real
for f being Function of REAL,REAL st f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) & (q - b) / (a - p) in A holds
f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])
let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) & (q - b) / (a - p) in A holds
f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])
let f be Function of REAL,REAL; :: thesis: ( f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) & (q - b) / (a - p) in A implies f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) )
assume A2: f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) ; :: thesis: ( not (q - b) / (a - p) in A or f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) )
assume (q - b) / (a - p) in A ; :: thesis: f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])
then (q - b) / (a - p) in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A4: ( lower_bound A <= (q - b) / (a - p) & (q - b) / (a - p) <= upper_bound A ) by XXREAL_1:1;
set F = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]);
A5: dom (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) = (dom ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).])) \/ (dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) by FUNCT_4:def 1
.= [.(lower_bound A),((q - b) / (a - p)).] \/ (dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) by FUNCT_2:def 1
.= [.(lower_bound A),((q - b) / (a - p)).] \/ [.((q - b) / (a - p)),(upper_bound A).] by FUNCT_2:def 1
.= [.(lower_bound A),(upper_bound A).] by XXREAL_1:165, A4
.= A by INTEGRA1:4
.= dom (f | A) by FUNCT_2:def 1 ;
for x being object st x in dom (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) holds
(((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x

proof

let x be object ; :: thesis: ( x in dom (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) implies (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x )
assume A6: x in dom (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) ; :: thesis: (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x
then reconsider x = x as Real by A5;
x in A by A6, A5;
then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A8: ( lower_bound A <= x & x <= upper_bound A ) by XXREAL_1:1;

per cases ( x < (q - b) / (a - p) or x >= (q - b) / (a - p) ) ;

suppose B1: x < (q - b) / (a - p) ; :: thesis: (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x

then B3: not x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by XXREAL_1:1;
B6: not x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) by XXREAL_1:236, B1;
B0: (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) . x by B3, FUNCT_4:11
.= (AffineMap (a,b)) . x by FUNCT_1:49, A8, B1, XXREAL_1:1
.= ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) . x by FUNCT_1:49, XXREAL_1:233, B1 ;
(f | A) . x = (((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[)) . x by A2, FUNCT_1:49, A6, A5;
hence (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x by B0, B6, FUNCT_4:11; :: thesis: verum

end;

suppose C1: x >= (q - b) / (a - p) ; :: thesis: (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x

then x in [.((q - b) / (a - p)),(upper_bound A).] by A8;
then C2: x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by FUNCT_2:def 1;
x in [.((q - b) / (a - p)),+infty.[ by XXREAL_1:236, C1;
then C3: x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) by FUNCT_2:def 1;
(((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) . x by C2, FUNCT_4:13
.= (AffineMap (p,q)) . x by FUNCT_1:49, A8, C1, XXREAL_1:1
.= ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) . x by FUNCT_1:49, XXREAL_1:236, C1
.= f . x by A2, FUNCT_4:13, C3 ;
hence (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x = (f | A) . x by FUNCT_1:49, A6, A5; :: thesis: verum

end;

end;

end;

hence f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by FUNCT_1:2, A5; :: thesis: verum