theorem :: AFINSQ_1:84

for x1, x2, x3, x4 being object holds len <%x1,x2,x3,x4%> = 4