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