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 ;
( 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*>)
;
(<*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
;
(<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . xthen <*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;
verum end; suppose A6:
x = 2
;
(<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . xthen <*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;
verum end; suppose A7:
x = 3
;
(<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . xthen <*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;
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; verum