let a be set ; :: thesis: for p being FinSequence holds len (p ^ <*a*>) = (len p) + 1
let p be FinSequence; :: thesis: len (p ^ <*a*>) = (len p) + 1
len (p ^ <*a*>) = (len p) + (len <*a*>) by FINSEQ_1:35;
hence len (p ^ <*a*>) = (len p) + 1 by FINSEQ_1:56; :: thesis: verum