<*P1,P2*> = <*P1*> ^ <*P2*> by FINSEQ_1:def 9;
hence <*P1,P2*> is Path-like ; :: thesis: verum