let D be non empty set ; :: thesis: for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*>
let p1, p2 be Element of D; :: thesis: Swap (<*p1,p2*>,1,2) = <*p2,p1*>
set f = <*p1,p2*>;
A1: len <*p1,p2*> = 2 by FINSEQ_1:44;
then 1 in dom <*p1,p2*> by FINSEQ_3:25;
then A2: <*p1,p2*> /. 1 = <*p1,p2*> . 1 by PARTFUN1:def 6
.= p1 ;
2 in dom <*p1,p2*> by A1, FINSEQ_3:25;
then A3: <*p1,p2*> /. 2 = <*p1,p2*> . 2 by PARTFUN1:def 6
.= p2 ;
Swap (<*p1,p2*>,1,2) = Replace ((Replace (<*p1,p2*>,1,(<*p1,p2*> /. 2))),2,(<*p1,p2*> /. 1)) by A1, Def2
.= Replace (<*p2,p2*>,2,(<*p1,p2*> /. 1)) by A3, Th13 ;
hence Swap (<*p1,p2*>,1,2) = <*p2,p1*> by A2, Th14; :: thesis: verum