set f = <*2,3,1*>;
set g = <*3,1,2*>;
rng <*2,3,1*> = {2,3,1} by FINSEQ_2:128
.= {1,2,3} by ENUMSET1:59 ;
then A1: ( dom <*2,3,1*> = {1,2,3} & rng <*2,3,1*> = dom <*3,1,2*> ) by FINSEQ_1:89, FINSEQ_3:1;
then A2: dom (<*3,1,2*> * <*2,3,1*>) = {1,2,3} by RELAT_1:27;
A3: for x being object 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 object ; :: thesis: ( x in dom (<*3,1,2*> * <*2,3,1*>) implies (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x )
assume A4: 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 A2, A4, ENUMSET1:def 1;

suppose A5: 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
.= 1
.= (id {1,2,3}) . x by A2, A4, A5, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; :: thesis: verum

end;

suppose A6: 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
.= 2
.= (id {1,2,3}) . x by A2, A4, A6, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; :: thesis: verum

end;

suppose A7: 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
.= 3
.= (id {1,2,3}) . x by A2, A4, A7, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; :: thesis: verum

end;

end;

end;

( <*2,3,1*> is one-to-one & dom (<*3,1,2*> * <*2,3,1*>) = dom (id {1,2,3}) ) by A2, FINSEQ_3:95, RELAT_1:45;
hence <*2,3,1*> " = <*3,1,2*> by A1, A3, FUNCT_1:2, FUNCT_1:41; :: thesis: verum