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