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%> . b1 = (id 2) . b1 )
assume x in dom <%0,1%> ; :: thesis: <%0,1%> . b1 = (id 2) . b1
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%> . b1 = (id 2) . b1
hence <%0,1%> . x = (id 2) . x by A2, FUNCT_1:18; :: thesis: verum
end;
suppose x = 1 ; :: thesis: <%0,1%> . b1 = (id 2) . b1
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