let p be FinSequence; :: thesis: for x, y, z being set st p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one holds
len p = 3
let x, y, z be set ; :: thesis: ( p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one implies len p = 3 )
( rng <*x,y,z*> = {x,y,z} & len <*x,y,z*> = 3 ) by FINSEQ_1:62, FINSEQ_2:148;
hence ( p is one-to-one & rng p = {x,y,z} & <*x,y,z*> is one-to-one implies len p = 3 ) by FINSEQ_1:65; :: thesis: verum