let i be Integer; :: thesis: for a being Real holds CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[)
let a be Real; :: 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 Lm18, RELAT_1:62;
dom (AffineMap (1,(- i))) = REAL by FUNCT_2:def 1;
then A2: dom ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) = ].(a + i),((a + i) + 1).[ by RELAT_1:62;
A3: for x being object 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 object ; :: 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 A4: 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 ;
y < (a + i) + 1 by A1, A4, XXREAL_1:4;
then A5: y - i < ((a + i) + 1) - i by XREAL_1:9;
a + i < y by A1, A4, XXREAL_1:4;
then (a + i) - i < y - i by XREAL_1:9;
then A6: y - i in ].a,(a + 1).[ by A5, 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, A2, A4, FUNCT_1:13
.= (CircleMap (R^1 a)) . ((AffineMap (1,(- i))) . x) by A1, A4, FUNCT_1:49
.= (CircleMap (R^1 a)) . ((1 * y) + (- i)) by FCONT_1:def 4
.= CircleMap . (y + (- i)) by A6, FUNCT_1:49
.= CircleMap . y by Th31
.= (CircleMap (R^1 (a + i))) . x by A1, A4, FUNCT_1:49 ; :: thesis: verum

end;

A7: rng ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) = ].a,(a + 1).[ by Lm24;
dom (CircleMap (R^1 a)) = ].a,(a + 1).[ by Lm18, RELAT_1:62;
then dom ((CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[)) = dom ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) by A7, RELAT_1:27;
hence CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) by A2, A3, Lm18, RELAT_1:62; :: thesis: verum