theorem Th46: :: FINSEQ_6:46

for D being non empty set
for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*> by Th45;