Lm1:
for x, y being element
for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
theorem
for
x1,
x2,
x3,
x4 being
set holds
len <%x1,x2,x3,x4%> = 4
theorem Th84:
for
x1,
x2,
x3,
x4 being
set holds
(
<%x1,x2,x3,x4%> . 0 = x1 &
<%x1,x2,x3,x4%> . 1
= x2 &
<%x1,x2,x3,x4%> . 2
= x3 &
<%x1,x2,x3,x4%> . 3
= x4 )
registration
let w,
x,
y,
z be
set ;
reducibility
<%w,x,y,z%> . 0 = w
by Th84;
reducibility
<%w,x,y,z%> . 1 = x
by Th84;
reducibility
<%w,x,y,z%> . 2 = y
by Th84;
reducibility
<%w,x,y,z%> . 3 = z
by Th84;
end;