let i be Element of NAT ; :: thesis: for y being set
for f being FinSubsequence st f = {[1,y]} holds
Shift (f,i) = {[(1 + i),y]}
let y be set ; :: thesis: for f being FinSubsequence st f = {[1,y]} holds
Shift (f,i) = {[(1 + i),y]}
let f be FinSubsequence; :: thesis: ( f = {[1,y]} implies Shift (f,i) = {[(1 + i),y]} )
set g = Shift (f,i);
assume A1: f = {[1,y]} ; :: thesis: 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)}
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(1 + i)} c= dom (Shift (f,i))
let x be object ; :: thesis: ( x in dom (Shift (f,i)) implies x in {(1 + i)} )
assume x in dom (Shift (f,i)) ; :: thesis: x in {(1 + i)}
then x in { (o + i) where o is Nat : o in dom f } by VALUED_1:def 12;
then consider w being Nat such that
A4: w + i = 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1 + i)} or x in dom (Shift (f,i)) )
assume x in {(1 + i)} ; :: thesis: x in dom (Shift (f,i))
then A6: x = 1 + i by TARSKI:def 1;
1 in dom f by A3, TARSKI:def 1;
then x in { (o + i) where o is Nat : o in dom f } by A6;
hence x in dom (Shift (f,i)) by VALUED_1:def 12; :: thesis: verum
end;
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; :: thesis: verum