let X, Y be set ; :: thesis: for f being FinSubsequence
for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
let f be FinSubsequence; :: thesis: for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
let n be Element of NAT ; :: thesis: ( ( for i being Nat holds
( i + n in X iff i in Y ) ) implies (n Shift f) | X = n Shift (f | Y) )
assume A1: for i being Nat holds
( i + n in X iff i in Y ) ; :: thesis: (n Shift f) | X = n Shift (f | Y)
set fY = f | Y;
set nf = n Shift f;
set nfX = (n Shift f) | X;
set nfY = n Shift (f | Y);
A2: dom (n Shift (f | Y)) = { (k + n) where k is Nat : k in dom (f | Y) } by VALUED_1:def 12;
A3: now :: thesis: for x being object st x in dom (n Shift (f | Y)) holds
((n Shift f) | X) . x = (n Shift (f | Y)) . x
let x be object ; :: thesis: ( x in dom (n Shift (f | Y)) implies ((n Shift f) | X) . x = (n Shift (f | Y)) . x )
assume x in dom (n Shift (f | Y)) ; :: thesis: ((n Shift f) | X) . x = (n Shift (f | Y)) . x
then consider k being Nat such that
A4: x = k + n and
A5: k in dom (f | Y) by A2;
A6: k in dom f by A5, RELAT_1:57;
A7: k in Y by A5, RELAT_1:57;
then x in X by A1, A4;
hence ((n Shift f) | X) . x = (n Shift f) . x by FUNCT_1:49
.= f . k by A4, A6, VALUED_1:def 12
.= (f | Y) . k by A7, FUNCT_1:49
.= (n Shift (f | Y)) . x by A4, A5, VALUED_1:def 12 ;
:: thesis: verum
end;
A8: dom (n Shift f) = { (k + n) where k is Nat : k in dom f } by VALUED_1:def 12;
A9: dom (n Shift (f | Y)) c= dom ((n Shift f) | X)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (n Shift (f | Y)) or x in dom ((n Shift f) | X) )
assume x in dom (n Shift (f | Y)) ; :: thesis: x in dom ((n Shift f) | X)
then consider k being Nat such that
A10: x = k + n and
A11: k in dom (f | Y) by A2;
k in Y by A11, RELAT_1:57;
then A12: x in X by A1, A10;
k in dom f by A11, RELAT_1:57;
then x in dom (n Shift f) by A8, A10;
hence x in dom ((n Shift f) | X) by A12, RELAT_1:57; :: thesis: verum
end;
dom ((n Shift f) | X) c= dom (n Shift (f | Y))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((n Shift f) | X) or x in dom (n Shift (f | Y)) )
assume A13: x in dom ((n Shift f) | X) ; :: thesis: x in dom (n Shift (f | Y))
then x in dom (n Shift f) by RELAT_1:57;
then consider k being Nat such that
A14: x = k + n and
A15: k in dom f by A8;
x in X by A13, RELAT_1:57;
then k in Y by A1, A14;
then k in dom (f | Y) by A15, RELAT_1:57;
hence x in dom (n Shift (f | Y)) by A2, A14; :: thesis: verum
end;
then dom (n Shift (f | Y)) = dom ((n Shift f) | X) by A9;
hence (n Shift f) | X = n Shift (f | Y) by A3, FUNCT_1:2; :: thesis: verum