let f be Function of 4,REAL; :: thesis: ex a, b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
reconsider a = f . 0, b = f . 1, c = f . 2, d = f . 3 as Element of REAL by XREAL_0:def 1;
take a ; :: thesis: ex b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
take b ; :: thesis: ex c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
take c ; :: thesis: ex d being Real st f = (0,1,2,3) --> (a,b,c,d)
take d ; :: thesis: f = (0,1,2,3) --> (a,b,c,d)
dom f = {0,1,2,3} by CARD_1:52, FUNCT_2:def 1;
hence f = (0,1,2,3) --> (a,b,c,d) by FUNCT_4:144; :: thesis: verum