theorem :: FINSEQ_3:37

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