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