let f be Function of 4,REAL; :: thesis: ex a, b, c, d being Element of 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 ;
take a ; :: thesis: ex b, c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
take b ; :: thesis: ex c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
take c ; :: thesis: ex d being Element of 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:90, FUNCT_2:def 1;
hence f = (0,1,2,3) --> (a,b,c,d) by Th6; :: thesis: verum