theorem :: FINSEQ_7:23

for D being non empty set
for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*>