A1: dom <%0,1%> = dom (id 2) by Th7, CARD_1:50;

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

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

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

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

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

end;

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

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

end;

end;

end;

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