theorem :: AFINSQ_1:50

for p being XFinSequence
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st p = (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%> holds
( len p = 9 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 )