let p be FinSequence; :: thesis: for x, y being object st p is one-to-one & rng p = {x,y} & x <> y holds
len p = 2
let x, y be object ; :: thesis: ( p is one-to-one & rng p = {x,y} & x <> y implies len p = 2 )
assume that
A1: p is one-to-one and
A2: rng p = {x,y} and
A3: x <> y ; :: thesis: len p = 2
set q = <*x,y*>;
A4: rng <*x,y*> = {x,y} by FINSEQ_2:127;
A5: len <*x,y*> = 2 by FINSEQ_1:44;
<*x,y*> is one-to-one by A3, Th92;
hence len p = 2 by A1, A2, A4, A5, FINSEQ_1:48; :: thesis: verum