let x be set ; :: thesis: for p being XFinSequence holds (p ^ <%x%>) . (len p) = x
let p be XFinSequence; :: thesis: (p ^ <%x%>) . (len p) = x
( dom <%x%> = 1 & 1 = 0 + 1 ) by Def5;
then A1: 0 in dom <%x%> by NAT_1:45;
(len p) + 0 = len p ;
hence (p ^ <%x%>) . (len p) = <%x%> . 0 by A1, Def4
.= x by Def5 ;
:: thesis: verum