let i be Element of NAT ; for y being set
for f being FinSubsequence st f = {[1,y]} holds
Shift (f,i) = {[(1 + i),y]}
let y be set ; for f being FinSubsequence st f = {[1,y]} holds
Shift (f,i) = {[(1 + i),y]}
let f be FinSubsequence; ( f = {[1,y]} implies Shift (f,i) = {[(1 + i),y]} )
set g = Shift (f,i);
assume A1:
f = {[1,y]}
; Shift (f,i) = {[(1 + i),y]}
then
card f = 1
by CARD_2:42;
then
card (Shift (f,i)) = 1
by VALUED_1:42;
then A2:
ex x being object st Shift (f,i) = {x}
by CARD_2:42;
A3:
dom f = {1}
by A1, RELAT_1:9;
dom (Shift (f,i)) = {(1 + i)}
then A7:
1 + i in dom (Shift (f,i))
by TARSKI:def 1;
1 in dom f
by A3, TARSKI:def 1;
then (Shift (f,i)) . (1 + i) =
f . 1
by VALUED_1:def 12
.=
y
by A1, GRFUNC_1:6
;
then
[(1 + i),y] in Shift (f,i)
by A7, FUNCT_1:def 2;
hence
Shift (f,i) = {[(1 + i),y]}
by A2, TARSKI:def 1; verum