let f be FinSequence; :: thesis: ( f is poorly-one-to-one implies Rev f is poorly-one-to-one )
assume A1: f is poorly-one-to-one ; :: thesis: Rev f is poorly-one-to-one
A2: len f = len (Rev f) by FINSEQ_5:def 3;

per cases ( len f <> 2 or len f = 2 ) ;

suppose A3: len f <> 2 ; :: thesis: Rev f is poorly-one-to-one

then f is weakly-one-to-one by A1, Th7;
then Rev f is weakly-one-to-one by Th9;
hence Rev f is poorly-one-to-one by A2, A3, Th7; :: thesis: verum

end;

suppose len f = 2 ; :: thesis: Rev f is poorly-one-to-one

hence Rev f is poorly-one-to-one by A2, Def3; :: thesis: verum

end;

end;