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

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

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

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

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

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

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

hence b in {x,y,z} by A2, ENUMSET1:def 1; :: thesis: verum

end;

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

hence b in {x,y,z} by A2, ENUMSET1:def 1; :: thesis: verum

end;

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

hence b in {x,y,z} by A2, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

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

per cases then ( b = x or b = y or b = z ) by ENUMSET1:def 1;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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