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: 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 Th22
.= (<*> D) ^ (CR /^ 0 )
.= CR /^ 0 by FINSEQ_1:47
.= CR by FINSEQ_5:31 ;
CR is_terminated_by CR by FINSEQ_8:28;
hence CR is_a_record_of <*> D,CR by A1, Def1; :: thesis: verum