let x, y, z be object ; <%x,y,z%> * <%2,1,0%> = <%z,y,x%>
rng <%2,1,0%> =
{2,1,0}
by Th8
.=
{0,1,2}
by ENUMSET1:60
.=
dom <%x,y,z%>
by Th8
;
then A1: dom (<%x,y,z%> * <%2,1,0%>) =
dom <%2,1,0%>
by RELAT_1:27
.=
{0,1,2}
by Th8
;
then A2:
dom (<%x,y,z%> * <%2,1,0%>) = dom <%z,y,x%>
by Th8;
now for a being object st a in dom (<%x,y,z%> * <%2,1,0%>) holds
(<%x,y,z%> * <%2,1,0%>) . a = <%z,y,x%> . alet a be
object ;
( a in dom (<%x,y,z%> * <%2,1,0%>) implies (<%x,y,z%> * <%2,1,0%>) . b1 = <%z,y,x%> . b1 )assume A3:
a in dom (<%x,y,z%> * <%2,1,0%>)
;
(<%x,y,z%> * <%2,1,0%>) . b1 = <%z,y,x%> . b1per cases then
( a = 0 or a = 1 or a = 2 )
by A1, ENUMSET1:def 1;
suppose A4:
a = 0
;
(<%x,y,z%> * <%2,1,0%>) . b1 = <%z,y,x%> . b1thus (<%x,y,z%> * <%2,1,0%>) . a =
<%x,y,z%> . (<%2,1,0%> . a)
by A3, FUNCT_1:12
.=
<%z,y,x%> . a
by A4
;
verum end; suppose A5:
a = 1
;
(<%x,y,z%> * <%2,1,0%>) . b1 = <%z,y,x%> . b1thus (<%x,y,z%> * <%2,1,0%>) . a =
<%x,y,z%> . (<%2,1,0%> . a)
by A3, FUNCT_1:12
.=
<%z,y,x%> . a
by A5
;
verum end; suppose A6:
a = 2
;
(<%x,y,z%> * <%2,1,0%>) . b1 = <%z,y,x%> . b1thus (<%x,y,z%> * <%2,1,0%>) . a =
<%x,y,z%> . (<%2,1,0%> . a)
by A3, FUNCT_1:12
.=
<%z,y,x%> . a
by A6
;
verum end; end;
hence
<%x,y,z%> * <%2,1,0%> = <%z,y,x%>
by A2, FUNCT_1:2; verum