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 () = 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 ;
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 ;
per cases ( ( f . 1 = 1 & f . 2 = 2 ) or ( f . 1 = 2 & f . 2 = 1 ) ) by ;
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 ;
hence f . x = x by A8; :: thesis: verum
end;
hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by ; :: 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 ;
hence f . x = (Rev (id (Seg 2))) . x by ; :: thesis: verum
end;
dom f = dom (Rev (id (Seg 2))) by ;
hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by ; :: thesis: verum
end;
end;