let x1, x2, x3, x4 be set ; :: thesis: ( <%x1,x2,x3,x4%> . 0 = x1 & <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
thus <%x1,x2,x3,x4%> . 0 = ((<%x1%> ^ <%x2,x3%>) ^ <%x4%>) . 0 by Th27
.= (<%x1%> ^ <%x2,x3,x4%>) . 0 by Th27
.= x1 by Th35 ; :: thesis: ( <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
A: len <%x1,x2,x3%> = 3 by Th39;
then B: 1 in dom <%x1,x2,x3%> by NAT_1:44;
thus <%x1,x2,x3,x4%> . 1 = <%x1,x2,x3%> . 1 by B, Def3
.= x2 by Th39 ; :: thesis: ( <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
C: 2 in dom <%x1,x2,x3%> by A, NAT_1:44;
thus <%x1,x2,x3,x4%> . 2 = <%x1,x2,x3%> . 2 by C, Def3
.= x3 by Th39 ; :: thesis: <%x1,x2,x3,x4%> . 3 = x4
thus <%x1,x2,x3,x4%> . 3 = x4 by A, Th36; :: thesis: verum