let i be Integer; 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; 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 ;
( 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)))
;
(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
;
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; verum