let r be Real; :: thesis: for p, q being FinSequence of REAL holds len ((p ^ <*r*>) ^ q) = ((len p) + (len q)) + 1
let p, q be FinSequence of REAL ; :: thesis: len ((p ^ <*r*>) ^ q) = ((len p) + (len q)) + 1
A1: len ((p ^ <*r*>) ^ q) = (len (p ^ <*r*>)) + (len q) by FINSEQ_1:22
.= ((len p) + (len <*r*>)) + (len q) by FINSEQ_1:22 ;
len <*r*> = 1 by FINSEQ_1:40;
hence len ((p ^ <*r*>) ^ q) = ((len p) + (len q)) + 1 by A1; :: thesis: verum