let p, q be XFinSequence; :: thesis: ( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q )
p c= p ^ q by Th78;
hence ( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by FUNCT_4:97, FUNCT_4:98; :: thesis: verum