let x1, x2, x3, x4 be object ; :: thesis: ( <%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 ; :: thesis: ( <%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 ; :: thesis: <%x1,x2,x3,x4%> . 3 = x4
thus <%x1,x2,x3,x4%> . 3 = x4 by A1, Th33; :: thesis: verum