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 ;
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 ;
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 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by ; :: 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 by FINSEQ_1:45
.= 2 by FINSEQ_1:45
.= (id {1,2,3}) . x by ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by ; :: 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 by FINSEQ_1:45
.= 3 by FINSEQ_1:45
.= (id {1,2,3}) . x by ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by ; :: 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 ;
hence <*2,3,1*> " = <*3,1,2*> by ; :: thesis: verum