let x1, x2 be object ; Rev <*x1,x2*> = <*x2,x1*>
set f = <*x1,x2*>;
set g = <*x2,x1*>;
A1:
len <*x1,x2*> = 2
by FINSEQ_1:44;
A2:
len <*x2,x1*> = 2
by FINSEQ_1:44;
now for i being Nat st i in dom <*x2,x1*> holds
<*x2,x1*> . i = <*x1,x2*> . (((len <*x1,x2*>) - i) + 1)let i be
Nat;
( i in dom <*x2,x1*> implies <*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1) )assume
i in dom <*x2,x1*>
;
<*x2,x1*> . b1 = <*x1,x2*> . (((len <*x1,x2*>) - b1) + 1)then A3:
i in Seg (len <*x1,x2*>)
by A1, A2, FINSEQ_1:def 3;
end;
hence
Rev <*x1,x2*> = <*x2,x1*>
by A1, A2, Def3; verum