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;

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;

end;

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

end;f . x = x

proof

hence
( f = id (Seg 2) or f = Rev (id (Seg 2)) )
by A2, FUNCT_1:17; :: thesis: verum
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;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

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

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

end;f . x = (Rev (id (Seg 2))) . x

proof

dom f = dom (Rev (id (Seg 2)))
by A1, A2, FINSEQ_5:57;
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;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

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