theorem :: FINSEQ_4:80

for ND being non empty set
for y1, y2, y3, y4 being Element of ND holds
( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 )