let w be FinSequence; :: thesis: for r being set
for i being Nat holds len (w +* i,r) = len w
let r be set ; :: thesis: for i being Nat holds len (w +* i,r) = len w
let i be Nat; :: thesis: len (w +* i,r) = len w
dom (w +* i,r) = dom w by Th32;
then Seg (len (w +* i,r)) = dom w by FINSEQ_1:def 3
.= Seg (len w) by FINSEQ_1:def 3 ;
hence len (w +* i,r) = len w by FINSEQ_1:8; :: thesis: verum