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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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