for p, q being XFinSequence holds
( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by Th71, FUNCT_4:97, FUNCT_4:98;