let w be FinSequence; :: thesis: for r being object
for i being natural Number holds len (w +* (i,r)) = len w
let r be object ; :: thesis: for i being natural Number holds len (w +* (i,r)) = len w
let i be natural Number ; :: thesis: len (w +* (i,r)) = len w
dom (w +* (i,r)) = dom w by Th29;
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:6; :: thesis: verum