set f = <*2,3,1*>;
set g = <*3,1,2*>;
A1: dom <*2,3,1*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
A2: <*2,3,1*> is one-to-one by FINSEQ_3:104;
rng <*2,3,1*> = {2,3,1} by FINSEQ_2:148
.= {1,2,3} by ENUMSET1:100 ;
then A3: rng <*2,3,1*> = dom <*3,1,2*> by FINSEQ_3:1, FINSEQ_3:30;
then A4: dom (<*3,1,2*> * <*2,3,1*>) = {1,2,3} by A1, RELAT_1:46;
then A5: dom (<*3,1,2*> * <*2,3,1*>) = dom (id {1,2,3}) by RELAT_1:71;
for x being set st x in dom (<*3,1,2*> * <*2,3,1*>) holds
(<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x

proof

let x be set ; :: thesis: ( x in dom (<*3,1,2*> * <*2,3,1*>) implies (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x )
assume A6: x in dom (<*3,1,2*> * <*2,3,1*>) ; :: thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x

per cases ( x = 1 or x = 2 or x = 3 ) by A4, A6, ENUMSET1:def 1;

suppose A7: x = 1 ; :: thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x

then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62
.= (id {1,2,3}) . x by A4, A6, A7, FUNCT_1:35 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A6, FUNCT_1:22; :: thesis: verum

end;

suppose A8: x = 2 ; :: thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x

then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62
.= (id {1,2,3}) . x by A4, A6, A8, FUNCT_1:35 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A6, FUNCT_1:22; :: thesis: verum

end;

suppose A9: x = 3 ; :: thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x

then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62
.= (id {1,2,3}) . x by A4, A6, A9, FUNCT_1:35 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A6, FUNCT_1:22; :: thesis: verum

end;

end;

end;

then <*3,1,2*> * <*2,3,1*> = id {1,2,3} by A5, FUNCT_1:9;
hence <*2,3,1*> " = <*3,1,2*> by A1, A2, A3, FUNCT_1:63; :: thesis: verum