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