let p be FinSequence; :: thesis: for x, y, z being object 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 object ; :: 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 and
A2: rng p = {x,y,z} and
A3: x <> y and
A4: y <> z and
A5: x <> z ; :: thesis: len p = 3
<*x,y,z*> is one-to-one by A3, A4, A5, Th93;
hence len p = 3 by A1, A2, Th98; :: thesis: verum