let i be Element of NAT ; :: thesis: for y being set
for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
let y be set ; :: thesis: for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}
let f be FinSubsequence; :: thesis: ( f = {[1,y]} implies i Shift f = {[(1 + i),y]} )
assume A1: f = {[1,y]} ; :: thesis: i Shift f = {[(1 + i),y]}
then card f = 1 by CARD_2:60;
then card (i Shift f) = 1 by PNPROC_1:57;
then consider x being set such that
A2: i Shift f = {x} by CARD_2:60;
set g = i Shift f;
A3: dom f = {1} by A1, RELAT_1:23;
dom (i Shift f) = {(1 + i)}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(1 + i)} c= dom (i Shift f)

let x be set ; :: thesis: ( x in dom (i Shift f) implies x in {(1 + i)} )
assume x in dom (i Shift f) ; :: thesis: x in {(1 + i)}
then x in { (i + o) where o is Element of NAT : o in dom f } by PNPROC_1:def 15;
then consider w being Element of NAT such that
A4: ( i + w = x & w in dom f ) ;
w = 1 by A3, A4, TARSKI:def 1;
hence x in {(1 + i)} by A4, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1 + i)} or x in dom (i Shift f) )
assume x in {(1 + i)} ; :: thesis: x in dom (i Shift f)
then A5: x = 1 + i by TARSKI:def 1;
1 in dom f by A3, TARSKI:def 1;
then x in { (i + o) where o is Element of NAT : o in dom f } by A5;
hence x in dom (i Shift f) by PNPROC_1:def 15; :: thesis: verum

end;

then A6: 1 + i in dom (i Shift f) by TARSKI:def 1;
1 in dom f by A3, TARSKI:def 1;
then (i Shift f) . (1 + i) = f . 1 by PNPROC_1:def 15
.= y by A1, GRFUNC_1:16 ;
then [(1 + i),y] in i Shift f by A6, FUNCT_1:def 4;
hence i Shift f = {[(1 + i),y]} by A2, TARSKI:def 1; :: thesis: verum