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:34;
hence ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) by FINSEQ_8:14; :: thesis: verum