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