let p be FinSequence; :: thesis: for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z holds
len p = 3
let x, y, z be set ; :: thesis: ( p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z implies len p = 3 )
assume that
A1: ( p is one-to-one & rng p = {x,y,z} ) and
A2: ( x <> y & y <> z & x <> z ) ; :: thesis: len p = 3
<*x,y,z*> is one-to-one by A2, Th104;
hence len p = 3 by A1, Th109; :: thesis: verum