let p be XFinSequence; :: thesis: 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 )
let x1, x2, x3, x4 be set ; :: thesis: ( p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> implies ( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 ) )
assume A1: p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> ; :: thesis: ( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
set p13 = (<%x1%> ^ <%x2%>) ^ <%x3%>;
A2: (<%x1%> ^ <%x2%>) ^ <%x3%> = <%x1,x2,x3%> ;
then A3: len ((<%x1%> ^ <%x2%>) ^ <%x3%>) = 3 by Th36;
A4: ( ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 0 = x1 & ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 1 = x2 ) by A2;
A5: ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 2 = x3 by A2;
thus len p = (len ((<%x1%> ^ <%x2%>) ^ <%x3%>)) + (len <%x4%>) by A1, Def3
.= 3 + 1 by A3, Th30
.= 4 ; :: thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
( 0 in 3 & 1 in 3 & 2 in 3 ) by CARD_1:51, ENUMSET1:def 1;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 ) by A1, A4, A5, Def3, A3; :: thesis: p . 3 = x4
thus p . 3 = p . (len ((<%x1%> ^ <%x2%>) ^ <%x3%>)) by A2, Th36
.= x4 by A1, Th33 ; :: thesis: verum