theorem :: FINSEQ_6:31

for x, y, z being set holds <*x,y,z*> |-- x = <*y,z*>