theorem Th15: :: QUATERNI:22

for f being Function of 4,REAL ex a, b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)