let x, y, z be set ; :: thesis: ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> )
len <*x,y,z*> = 3 by FINSEQ_1:45;
hence ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> ) by FINSEQ_3:25; :: thesis: verum