let x be set ; :: 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:35
.= 1 + (len f) by FINSEQ_1:56 ; :: thesis: verum