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:45;
assume that
A2: dom f = Seg 2 and
A3: rng f = Seg 2 ; :: thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )
A4: 1 in dom f by A2;
then f . 1 in rng f by FUNCT_1:3;
then A5: ( f . 1 = 1 or f . 1 = 2 ) by A3, FINSEQ_1:2, TARSKI:def 2;
A6: 2 in dom f by A2;
then f . 2 in rng f by FUNCT_1:3;
then A7: ( f . 2 = 2 or f . 2 = 1 ) by A3, FINSEQ_1:2, TARSKI:def 2;

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

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

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

proof

let x be object ; :: 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:2, TARSKI:def 2;
hence f . x = x by A8; :: thesis: verum

end;

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

end;

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

A10: for x being object st x in Seg 2 holds
f . x = (Rev (id (Seg 2))) . x

proof

let x be object ; :: 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:2, TARSKI:def 2;
hence f . x = (Rev (id (Seg 2))) . x by A9, Th2; :: thesis: verum

end;

dom f = dom (Rev (id (Seg 2))) by A1, A2, FINSEQ_5:57;
hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by A2, A10, FUNCT_1:2; :: thesis: verum

end;

end;