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