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

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

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

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

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

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

end;

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

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

end;

end;

end;

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