let D be non empty set ; :: thesis: for p1, p2, p3 being Element of D holds Swap <*p1,p2,p3*>,1,3 = <*p3,p2,p1*>
let p1, p2, p3 be Element of D; :: thesis: Swap <*p1,p2,p3*>,1,3 = <*p3,p2,p1*>
set f = <*p1,p2,p3*>;
A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:62;
then 1 in dom <*p1,p2,p3*> by FINSEQ_3:27;
then A2: <*p1,p2,p3*> /. 1 = <*p1,p2,p3*> . 1 by PARTFUN1:def 8
.= p1 by FINSEQ_1:62 ;
3 in dom <*p1,p2,p3*> by A1, FINSEQ_3:27;
then A3: <*p1,p2,p3*> /. 3 = <*p1,p2,p3*> . 3 by PARTFUN1:def 8
.= p3 by FINSEQ_1:62 ;
Swap <*p1,p2,p3*>,1,3 = Replace (Replace <*p1,p2,p3*>,1,(<*p1,p2,p3*> /. 3)),3,(<*p1,p2,p3*> /. 1) by A1, Def2
.= Replace <*p3,p2,p3*>,3,(<*p1,p2,p3*> /. 1) by A3, Th17 ;
hence Swap <*p1,p2,p3*>,1,3 = <*p3,p2,p1*> by A2, Th19; :: thesis: verum