let x, y be object ; :: thesis: ( dom <%x,y%> = {0,1} & rng <%x,y%> = {x,y} )
thus A1: dom <%x,y%> = {0,1} by Th35, CARD_1:50; :: thesis: rng <%x,y%> = {x,y}

now :: thesis: for b being object holds
( ( b in rng <%x,y%> implies b in {x,y} ) & ( b in {x,y} implies b in rng <%x,y%> ) )

let b be object ; :: thesis: ( ( b in rng <%x,y%> implies b in {x,y} ) & ( b in {x,y} implies b₁ in rng <%x,y%> ) )

hereby :: thesis: ( b in {x,y} implies b₁ in rng <%x,y%> )

assume b in rng <%x,y%> ; :: thesis: b in {x,y}
then consider a being object such that
A2: ( a in dom <%x,y%> & <%x,y%> . a = b ) by FUNCT_1:def 3;

per cases ( a = 0 or a = 1 ) by A1, A2, TARSKI:def 2;

suppose a = 0 ; :: thesis: b in {x,y}

hence b in {x,y} by A2, TARSKI:def 2; :: thesis: verum

end;

suppose a = 1 ; :: thesis: b in {x,y}

hence b in {x,y} by A2, TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume b in {x,y} ; :: thesis: b₁ in rng <%x,y%>

per cases then ( b = x or b = y ) by TARSKI:def 2;

suppose b = x ; :: thesis: b₁ in rng <%x,y%>

then ( 0 in dom <%x,y%> & <%x,y%> . 0 = b ) by A1, TARSKI:def 2;
hence b in rng <%x,y%> by FUNCT_1:3; :: thesis: verum

end;

suppose b = y ; :: thesis: b₁ in rng <%x,y%>

then ( 1 in dom <%x,y%> & <%x,y%> . 1 = b ) by A1, TARSKI:def 2;
hence b in rng <%x,y%> by FUNCT_1:3; :: thesis: verum

end;

end;

end;

hence rng <%x,y%> = {x,y} by TARSKI:2; :: thesis: verum