let p be FinSequence; :: thesis: for x, y being set st p is one-to-one & rng p = {x,y} & x <> y holds
len p = 2
let x, y be set ; :: thesis: ( p is one-to-one & rng p = {x,y} & x <> y implies len p = 2 )
assume that
A1: ( p is one-to-one & rng p = {x,y} ) and
A2: x <> y ; :: thesis: len p = 2
set q = <*x,y*>;
( rng <*x,y*> = {x,y} & <*x,y*> is one-to-one & len <*x,y*> = 2 ) by A2, Th103, FINSEQ_1:61, FINSEQ_2:147;
hence len p = 2 by A1, FINSEQ_1:65; :: thesis: verum