theorem Th19: :: FINSEQ_6:19

for p1, p2 being set holds p1 .. <*p1,p2*> = 1