let D be non empty set ; :: thesis: for CR being FinSequence of D holds CR is_a_record_of <*> D,CR
let CR be FinSequence of D; :: thesis: CR is_a_record_of <*> D,CR
A1: CR is_terminated_by CR by FINSEQ_8:28;
addcr ((<*> D),CR) = ovlcon ((<*> D),CR) by FINSEQ_8:def 11
.= (<*> D) ^ (CR /^ (len (ovlpart ((<*> D),CR)))) by FINSEQ_8:def 3
.= (<*> D) ^ (CR /^ (len (<*> D))) by Th21
.= (<*> D) ^ (CR /^ 0)
.= CR /^ 0 by FINSEQ_1:34
.= CR ;
hence CR is_a_record_of <*> D,CR by A1; :: thesis: verum