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

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