let D be non empty set ; for p1, p2 being Element of D holds Swap <*p1,p2*>,1,2 = <*p2,p1*>
let p1, p2 be Element of D; Swap <*p1,p2*>,1,2 = <*p2,p1*>
set f = <*p1,p2*>;
A1:
len <*p1,p2*> = 2
by FINSEQ_1:61;
then
1 in dom <*p1,p2*>
by FINSEQ_3:27;
then A2: <*p1,p2*> /. 1 =
<*p1,p2*> . 1
by PARTFUN1:def 8
.=
p1
by FINSEQ_1:61
;
2 in dom <*p1,p2*>
by A1, FINSEQ_3:27;
then A3: <*p1,p2*> /. 2 =
<*p1,p2*> . 2
by PARTFUN1:def 8
.=
p2
by FINSEQ_1:61
;
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, Th15
;
hence
Swap <*p1,p2*>,1,2 = <*p2,p1*>
by A2, Th16; verum