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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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