let x1, x2, x3, x4 be object ; ( <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
A1:
len <%x1,x2,x3%> = 3
by Th36;
then A2:
1 in dom <%x1,x2,x3%>
by Lm1;
thus <%x1,x2,x3,x4%> . 1 =
<%x1,x2,x3%> . 1
by A2, Def3
.=
x2
; ( <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
A3:
2 in dom <%x1,x2,x3%>
by A1, Lm1;
thus <%x1,x2,x3,x4%> . 2 =
<%x1,x2,x3%> . 2
by A3, Def3
.=
x3
; <%x1,x2,x3,x4%> . 3 = x4
thus
<%x1,x2,x3,x4%> . 3 = x4
by A1, Th33; verum