theorem Th42: :: AFINSQ_1:45

for p being XFinSequence
for x1, x2, x3, x4 being set st p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> holds
( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )