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