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 )
A1: len <*x,y,z*> = 3 by FINSEQ_1:62;
rng <*x,y,z*> = {x,y,z} by 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 A1, FINSEQ_1:65; :: thesis: verum