let p be FinSequence; :: thesis: for x, y, z being object 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 object ; :: 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:45;
rng <*x,y,z*> = {x,y,z} by FINSEQ_2:128;
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:48; :: thesis: verum