let f be one-to-one Function; :: thesis: ( dom f = Seg 2 & rng f = Seg 2 & not f = id (Seg 2) implies f = Rev (id (Seg 2)) )
A1: dom (idseq 2) = Seg 2 by RELAT_1:71;
assume A2: ( dom f = Seg 2 & rng f = Seg 2 ) ; :: thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )
then A3: 1 in dom f ;
then f . 1 in rng f by FUNCT_1:12;
then A4: ( f . 1 = 1 or f . 1 = 2 ) by A2, FINSEQ_1:4, TARSKI:def 2;
A5: 2 in dom f by A2;
then f . 2 in rng f by FUNCT_1:12;
then A6: ( f . 2 = 2 or f . 2 = 1 ) by A2, FINSEQ_1:4, TARSKI:def 2;

per cases ( ( f . 1 = 1 & f . 2 = 2 ) or ( f . 1 = 2 & f . 2 = 1 ) ) by A3, A4, A5, A6, FUNCT_1:def 8;

suppose A7: ( f . 1 = 1 & f . 2 = 2 ) ; :: thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )

for x being set st x in Seg 2 holds
f . x = x

proof

let x be set ; :: thesis: ( x in Seg 2 implies f . x = x )
assume x in Seg 2 ; :: thesis: f . x = x
then ( x = 1 or x = 2 ) by FINSEQ_1:4, TARSKI:def 2;
hence f . x = x by A7; :: thesis: verum

end;

hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by A2, FUNCT_1:34; :: thesis: verum

end;

suppose A8: ( f . 1 = 2 & f . 2 = 1 ) ; :: thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )

A9: dom f = dom (Rev (id (Seg 2))) by A1, A2, FINSEQ_5:60;
for x being set st x in Seg 2 holds
f . x = (Rev (id (Seg 2))) . x

proof

let x be set ; :: thesis: ( x in Seg 2 implies f . x = (Rev (id (Seg 2))) . x )
assume x in Seg 2 ; :: thesis: f . x = (Rev (id (Seg 2))) . x
then ( x = 1 or x = 2 ) by FINSEQ_1:4, TARSKI:def 2;
hence f . x = (Rev (id (Seg 2))) . x by A8, Th2; :: thesis: verum

end;

hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by A2, A9, FUNCT_1:9; :: thesis: verum

end;

end;