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 ;
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 ;
then A5: y - i < ((a + i) + 1) - i by XREAL_1:9;
a + i < y by ;
then (a + i) - i < y - i by XREAL_1:9;
then A6: y - i in ].a,(a + 1).[ by ;
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
.= (CircleMap (R^1 a)) . ((AffineMap (1,(- i))) . x) by
.= (CircleMap (R^1 a)) . ((1 * y) + (- i)) by FCONT_1:def 4
.= CircleMap . (y + (- i)) by
.= CircleMap . y by Th31
.= (CircleMap (R^1 (a + i))) . x by ; :: 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 ;
then dom ((CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[)) = dom ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) by ;
hence CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[) by ; :: thesis: verum