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

hence <*2,3,1*> " = <*3,1,2*> by A1, A3, FUNCT_1:2, FUNCT_1:41; :: thesis: verum

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

( <*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;
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

end;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;

end;

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
by FINSEQ_1:45

.= 1 by FINSEQ_1:45

.= (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;.= 1 by FINSEQ_1:45

.= (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

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
by FINSEQ_1:45

.= 2 by FINSEQ_1:45

.= (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;.= 2 by FINSEQ_1:45

.= (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

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
by FINSEQ_1:45

.= 3 by FINSEQ_1:45

.= (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;.= 3 by FINSEQ_1:45

.= (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

hence <*2,3,1*> " = <*3,1,2*> by A1, A3, FUNCT_1:2, FUNCT_1:41; :: thesis: verum