A1: dom <%0,1,2%> = dom (id 3) by Th8, CARD_1:51;

now :: thesis: for x being object st x in dom <%0,1,2%> holds
<%0,1,2%> . x = (id 3) . x

let x be object ; :: thesis: ( x in dom <%0,1,2%> implies <%0,1,2%> . b₁ = (id 3) . b₁ )
assume x in dom <%0,1,2%> ; :: thesis: <%0,1,2%> . b₁ = (id 3) . b₁
then A2: ( x in 3 & x in {0,1,2} ) by A1, Th8;

per cases then ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def 1;

suppose x = 0 ; :: thesis: <%0,1,2%> . b₁ = (id 3) . b₁

hence <%0,1,2%> . x = (id 3) . x by A2, FUNCT_1:18; :: thesis: verum

end;

suppose x = 1 ; :: thesis: <%0,1,2%> . b₁ = (id 3) . b₁

hence <%0,1,2%> . x = (id 3) . x by A2, FUNCT_1:18; :: thesis: verum

end;

suppose x = 2 ; :: thesis: <%0,1,2%> . b₁ = (id 3) . b₁

hence <%0,1,2%> . x = (id 3) . x by A2, FUNCT_1:18; :: thesis: verum

end;

end;

end;

hence <%0,1,2%> = id 3 by A1, FUNCT_1:2; :: thesis: verum