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]} )
set g = i Shift f;
assume A1: f = {[1,y]} ; :: thesis: i Shift f = {[(1 + i),y]}
then card f = 1 by CARD_2:42;
then card (i Shift f) = 1 by PNPROC_1:54;
then A2: ex x being set st i Shift f = {x} by CARD_2:42;
A3: dom f = {1} by A1, RELAT_1:9;
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 14;
then consider w being Element of NAT such that
A4: i + w = x and
A5: w in dom f ;
w = 1 by A3, A5, 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 A6: 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 A6;
hence x in dom (i Shift f) by PNPROC_1:def 14; :: thesis: verum

end;

then A7: 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 14
.= y by A1, GRFUNC_1:6 ;
then [(1 + i),y] in i Shift f by A7, FUNCT_1:def 2;
hence i Shift f = {[(1 + i),y]} by A2, TARSKI:def 1; :: thesis: verum