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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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