let x be object ; :: thesis: for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)
let f be FinSequence; :: thesis: len (<*x*> ^ f) = 1 + (len f)
thus len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22
.= 1 + (len f) by FINSEQ_1:39 ; :: thesis: verum