let D be set ; :: thesis: for f being XFinSequence of D holds dom (Shift (f,1)) = Seg (len f)
let f be XFinSequence of D; :: thesis: dom (Shift (f,1)) = Seg (len f)
A1: for x being object st x in Seg (len f) holds
x in dom (Shift (f,1))

proof

let x be object ; :: thesis: ( x in Seg (len f) implies x in dom (Shift (f,1)) )
assume B1: x in Seg (len f) ; :: thesis: x in dom (Shift (f,1))
then reconsider x = x as Nat ;
x >= 1 by B1, FINSEQ_1:1;
then reconsider y = x - 1 as Nat ;
y + 1 in Seg (len f) by B1;
then y in Segm (len f) by NEWTON02:106;
then y + 1 in dom (Shift (f,1)) by VALUED_1:24;
hence x in dom (Shift (f,1)) ; :: thesis: verum

end;

for x being object st x in dom (Shift (f,1)) holds
x in Seg (len f)

proof

let x be object ; :: thesis: ( x in dom (Shift (f,1)) implies x in Seg (len f) )
assume B1: x in dom (Shift (f,1)) ; :: thesis: x in Seg (len f)
then reconsider x = x as Nat ;
consider y being Nat such that
B2: ( y in dom f & x = y + 1 ) by B1, VALUED_1:39;
y in Segm (len f) by B2;
hence x in Seg (len f) by B2, NEWTON02:106; :: thesis: verum

end;

hence dom (Shift (f,1)) = Seg (len f) by A1, TARSKI:2; :: thesis: verum