let f be Function of 2,REAL ; :: thesis: ex a, b being Element of REAL st f = 0 ,1 --> a,b
( 0 in 2 & 1 in 2 ) by CARD_1:88, TARSKI:def 2;
then reconsider a = f . 0 , b = f . 1 as Element of REAL by FUNCT_2:7;
take a ; :: thesis: ex b being Element of REAL st f = 0 ,1 --> a,b
take b ; :: thesis: f = 0 ,1 --> a,b
dom f = {0 ,1} by CARD_1:88, FUNCT_2:def 1;
hence f = 0 ,1 --> a,b by FUNCT_4:69; :: thesis: verum