let p be FinSequence; :: thesis: for x being object holds (p ^ <*x*>) . ((len p) + 1) = x
let x be object ; :: 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 ;
:: thesis: verum