theorem :: FINSEQ_3:36

for u, x, y, z being object holds <*u*> <> <*x,y,z*>