let a be object ; :: 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:22;
hence len (p ^ <*a*>) = (len p) + 1 by FINSEQ_1:39; :: thesis: verum