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