let x, y, z be object ; :: thesis: <%x,y,z%> * <%2,0,1%> = <%z,x,y%>
rng <%2,0,1%> = {2,0,1} by Th8
.= {2,1,0} by ENUMSET1:57
.= {0,1,2} by ENUMSET1:60
.= dom <%x,y,z%> by Th8 ;
then A1: dom (<%x,y,z%> * <%2,0,1%>) = dom <%2,0,1%> by RELAT_1:27
.= {0,1,2} by Th8 ;
then A2: dom (<%x,y,z%> * <%2,0,1%>) = dom <%z,x,y%> by Th8;

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

let a be object ; :: thesis: ( a in dom (<%x,y,z%> * <%2,0,1%>) implies (<%x,y,z%> * <%2,0,1%>) . b₁ = <%z,x,y%> . b₁ )
assume A3: a in dom (<%x,y,z%> * <%2,0,1%>) ; :: thesis: (<%x,y,z%> * <%2,0,1%>) . b₁ = <%z,x,y%> . b₁

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

suppose A4: a = 0 ; :: thesis: (<%x,y,z%> * <%2,0,1%>) . b₁ = <%z,x,y%> . b₁

thus (<%x,y,z%> * <%2,0,1%>) . a = <%x,y,z%> . (<%2,0,1%> . a) by A3, FUNCT_1:12
.= <%z,x,y%> . a by A4 ; :: thesis: verum

end;

suppose A5: a = 1 ; :: thesis: (<%x,y,z%> * <%2,0,1%>) . b₁ = <%z,x,y%> . b₁

thus (<%x,y,z%> * <%2,0,1%>) . a = <%x,y,z%> . (<%2,0,1%> . a) by A3, FUNCT_1:12
.= <%z,x,y%> . a by A5 ; :: thesis: verum

end;

suppose A6: a = 2 ; :: thesis: (<%x,y,z%> * <%2,0,1%>) . b₁ = <%z,x,y%> . b₁

thus (<%x,y,z%> * <%2,0,1%>) . a = <%x,y,z%> . (<%2,0,1%> . a) by A3, FUNCT_1:12
.= <%z,x,y%> . a by A6 ; :: thesis: verum

end;

end;

end;

hence <%x,y,z%> * <%2,0,1%> = <%z,x,y%> by A2, FUNCT_1:2; :: thesis: verum