let f be Function of 2,REAL; 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
; ex b being Element of REAL st f = (0,1) --> (a,b)
take
b
; 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; verum