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:50, TARSKI:def 2;
then reconsider a = f . 0, b = f . 1 as Element of REAL by FUNCT_2:5;
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:50, FUNCT_2:def 1;
hence f = (0,1) --> (a,b) by FUNCT_4:66; :: thesis: verum