let x1, x2 be object ; :: thesis: 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 :: thesis: 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; :: thesis: ( i in dom <*x2,x1*> implies <*x2,x1*> . b₁ = <*x1,x2*> . (((len <*x1,x2*>) - b₁) + 1) )
assume i in dom <*x2,x1*> ; :: thesis: <*x2,x1*> . b₁ = <*x1,x2*> . (((len <*x1,x2*>) - b₁) + 1)
then A3: i in Seg (len <*x1,x2*>) by A1, A2, FINSEQ_1:def 3;

per cases ( i = 1 or i = 2 ) by A1, A3, FINSEQ_1:2, TARSKI:def 2;

suppose A4: i = 1 ; :: thesis: <*x2,x1*> . b₁ = <*x1,x2*> . (((len <*x1,x2*>) - b₁) + 1)

hence <*x2,x1*> . i = x2
.= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A4 ;
:: thesis: verum

end;

suppose A5: i = 2 ; :: thesis: <*x2,x1*> . b₁ = <*x1,x2*> . (((len <*x1,x2*>) - b₁) + 1)

hence <*x2,x1*> . i = x1
.= <*x1,x2*> . (((len <*x1,x2*>) - i) + 1) by A1, A5 ;
:: thesis: verum

end;

end;

end;

hence Rev <*x1,x2*> = <*x2,x1*> by A1, A2, Def3; :: thesis: verum