let i be Integer; :: thesis: for a being real number holds CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)
let a be real number ; :: thesis: CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)
set W = ].a,(a + 1).[;
set Q = ].(a + i),((a + i) + 1).[;
set h = CircleMap (R^1 (a + i));
set g = CircleMap (R^1 a);
set F = AffineMap 1,(- i);
set f = (AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[;
A1: dom (CircleMap (R^1 (a + i))) = ].(a + i),((a + i) + 1).[ by Lm19, RELAT_1:91;
A2: dom (CircleMap (R^1 a)) = ].a,(a + 1).[ by Lm19, RELAT_1:91;
dom (AffineMap 1,(- i)) = REAL by FUNCT_2:def 1;
then A3: dom ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[) = ].(a + i),((a + i) + 1).[ by RELAT_1:91;
rng ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[) = ].a,(a + 1).[ by Lm26;
then A4: dom ((CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)) = dom ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[) by A2, RELAT_1:46;
for x being set st x in dom (CircleMap (R^1 (a + i))) holds
(CircleMap (R^1 (a + i))) . x = ((CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)) . x

proof

let x be set ; :: thesis: ( x in dom (CircleMap (R^1 (a + i))) implies (CircleMap (R^1 (a + i))) . x = ((CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)) . x )
assume A5: x in dom (CircleMap (R^1 (a + i))) ; :: thesis: (CircleMap (R^1 (a + i))) . x = ((CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)) . x
then reconsider y = x as Real by A1;
( a + i < y & y < (a + i) + 1 ) by A1, A5, XXREAL_1:4;
then ( (a + i) - i < y - i & y - i < ((a + i) + 1) - i ) by XREAL_1:11;
then A6: y - i in ].a,(a + 1).[ by XXREAL_1:4;
thus ((CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[)) . x = (CircleMap (R^1 a)) . (((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[) . x) by A1, A3, A5, FUNCT_1:23
.= (CircleMap (R^1 a)) . ((AffineMap 1,(- i)) . x) by A1, A5, FUNCT_1:72
.= (CircleMap (R^1 a)) . ((1 * y) + (- i)) by JORDAN16:def 3
.= CircleMap . (y + (- i)) by A6, FUNCT_1:72
.= CircleMap . y by Th32
.= (CircleMap (R^1 (a + i))) . x by A1, A5, FUNCT_1:72 ; :: thesis: verum

end;

hence CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap 1,(- i)) | ].(a + i),((a + i) + 1).[) by A1, A3, A4, FUNCT_1:9; :: thesis: verum