theorem Th8: :: AMI_8:8

for x1, x2, x3, x4, x5, x6 being object
for f being Function st <%x1,x2,x3,x4,x5,x6%> c= f holds
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 )