theorem :: FINSEQ_1:43

for x, y, z being object holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th32;