let x be set ; :: thesis: for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x
let p be FinSequence; :: thesis: (p ^ <*x*>) . ((len p) + 1) = x
dom <*x*> = Seg 1 by Def8;
then 1 in dom <*x*> ;
hence (p ^ <*x*>) . ((len p) + 1) = <*x*> . 1 by Def7
.= x by Def8 ;
:: thesis: verum