let D be non empty set ; :: thesis: for r being FinSequence of D holds
( ovlpart (<*> D),r = <*> D & ovlpart r,(<*> D) = <*> D )
let r be FinSequence of D; :: thesis: ( ovlpart (<*> D),r = <*> D & ovlpart r,(<*> D) = <*> D )
( (<*> D) ^ r = r & r ^ (<*> D) = r ) by FINSEQ_1:47;
hence ( ovlpart (<*> D),r = <*> D & ovlpart r,(<*> D) = <*> D ) by FINSEQ_8:14; :: thesis: verum