let p be XFinSequence; :: thesis: for x1, x2, x3, x4, x5, x6 being set st p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> holds
( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
let x1, x2, x3, x4, x5, x6 be set ; :: thesis: ( p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> implies ( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 ) )
assume A1: p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> ; :: thesis: ( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
set p15 = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>;
A2: len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) = 5 by Th43;
A3: ( ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 0 = x1 & ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 1 = x2 ) by Th43;
A4: ( ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 2 = x3 & ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 3 = x4 ) by Th43;
A5: ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 4 = x5 by Th43;
thus len p = (len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>)) + (len <%x6%>) by A1, Def3
.= 5 + 1 by A2, Th30
.= 6 ; :: thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
0 in 5 & ... & 4 in 5 by CARD_1:53, ENUMSET1:def 3;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 ) by A1, A3, A4, A5, Def3, A2; :: thesis: p . 5 = x6
thus p . 5 = p . (len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>)) by Th43
.= x6 by A1, Th33 ; :: thesis: verum