theorem Th74: :: FINSEQ_4:74

for x1, x2, x3, x4 being object holds
( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )