theorem :: FINSEQ_7:25

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