set f = <*1,3,2*>;
set g = <*2,1,3*>;
set h = <*3,2,1*>;
set F = <*2,3,1*>;
set G = <*3,1,2*>;
dom <*1,3,2*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then A1: ( 1 in dom <*1,3,2*> & 2 in dom <*1,3,2*> & 3 in dom <*1,3,2*> ) by ENUMSET1:def 1;
dom <*2,3,1*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then A2: ( 1 in dom <*2,3,1*> & 2 in dom <*2,3,1*> & 3 in dom <*2,3,1*> ) by ENUMSET1:def 1;
dom <*2,1,3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then A3: ( 1 in dom <*2,1,3*> & 2 in dom <*2,1,3*> & 3 in dom <*2,1,3*> ) by ENUMSET1:def 1;
dom <*3,1,2*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then A4: ( 1 in dom <*3,1,2*> & 2 in dom <*3,1,2*> & 3 in dom <*3,1,2*> ) by ENUMSET1:def 1;
dom <*3,2,1*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then A5: ( 1 in dom <*3,2,1*> & 2 in dom <*3,2,1*> & 3 in dom <*3,2,1*> ) by ENUMSET1:def 1;
A6: ( <*2,1,3*> is Permutation of (Seg 3) & <*3,2,1*> is Permutation of (Seg 3) & <*2,3,1*> is Permutation of (Seg 3) & <*3,1,2*> is Permutation of (Seg 3) & <*1,3,2*> is Permutation of (Seg 3) ) by Th27, MATRIX_2:def 11;
A7: <*1,3,2*> is Permutation of (Seg 3) by Th27, MATRIX_2:def 11;
reconsider f = <*1,3,2*>, g = <*2,1,3*>, h = <*3,2,1*>, F = <*2,3,1*>, G = <*3,1,2*> as FinSequence of Seg 3 by A6, Th36;
A8: ( 3 = len h & 3 = len g & 3 = len f & 3 = len F & 3 = len G ) by FINSEQ_1:62;
then reconsider gf = g * f as FinSequence of Seg 3 by A7, FINSEQ_2:50;
A9: ( f is Permutation of (Seg 3) & g is Permutation of (Seg 3) & h is Permutation of (Seg 3) & G is Permutation of (Seg 3) & F is Permutation of (Seg 3) ) by Th27, MATRIX_2:def 11;
then A10: len gf = 3 by A8, FINSEQ_2:47;
reconsider fg = f * g as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A11: len fg = 3 by A8, A9, FINSEQ_2:47;
reconsider fF = f * F as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A12: len fF = 3 by A8, A9, FINSEQ_2:47;
reconsider fh = f * h as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A13: len fh = 3 by A8, A9, FINSEQ_2:47;
reconsider hf = h * f as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A14: len hf = 3 by A8, A9, FINSEQ_2:47;
reconsider FF = F * F as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A15: len FF = 3 by A8, A9, FINSEQ_2:47;
reconsider FG = F * G as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A16: len FG = 3 by A8, A9, FINSEQ_2:47;
reconsider GF = G * F as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A17: len GF = 3 by A8, A9, FINSEQ_2:47;
reconsider GG = G * G as FinSequence of Seg 3 by A6, A8, FINSEQ_2:50;
A18: len GG = 3 by A8, A9, FINSEQ_2:47;
reconsider gh = g * h as FinSequence of Seg 3 by A8, A9, FINSEQ_2:50;
A19: len gh = 3 by A8, A9, FINSEQ_2:47;
reconsider hg = h * g as FinSequence of Seg 3 by A8, A9, FINSEQ_2:50;
A20: len hg = 3 by A8, A9, FINSEQ_2:47;
reconsider hh = h * h as FinSequence of Seg 3 by A8, A9, FINSEQ_2:50;
A21: len hh = 3 by A8, A9, FINSEQ_2:47;
reconsider gg = g * g as FinSequence of Seg 3 by A8, A9, FINSEQ_2:50;
A22: len gg = 3 by A8, A9, FINSEQ_2:47;
reconsider ff = f * f as FinSequence of Seg 3 by A8, A9, FINSEQ_2:50;
A23: len ff = 3 by A8, A9, FINSEQ_2:47;
thus <*2,1,3*> * <*1,3,2*> = <*2,3,1*> :: thesis: ( <*1,3,2*> * <*2,1,3*> = <*3,1,2*> & <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A24: gf . 1 = g . (f . 1) by A1, FUNCT_1:23
.= g . 1 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
A25: gf . 2 = g . (f . 2) by A1, FUNCT_1:23
.= g . 3 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
gf . 3 = g . (f . 3) by A1, FUNCT_1:23
.= g . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hence <*2,1,3*> * <*1,3,2*> = <*2,3,1*> by A10, A24, A25, FINSEQ_1:62; :: thesis: verum

end;

thus <*1,3,2*> * <*2,1,3*> = <*3,1,2*> :: thesis: ( <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A26: fg . 1 = f . (g . 1) by A3, FUNCT_1:23
.= f . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
A27: fg . 2 = f . (g . 2) by A3, FUNCT_1:23
.= f . 1 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
fg . 3 = f . (g . 3) by A3, FUNCT_1:23
.= f . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
hence <*1,3,2*> * <*2,1,3*> = <*3,1,2*> by A11, A26, A27, FINSEQ_1:62; :: thesis: verum

end;

thus <*2,1,3*> * <*3,2,1*> = <*3,1,2*> :: thesis: ( <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A28: gh . 1 = g . (h . 1) by A5, FUNCT_1:23
.= g . 3 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
A29: gh . 2 = g . (h . 2) by A5, FUNCT_1:23
.= g . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
gh . 3 = g . (h . 3) by A5, FUNCT_1:23
.= g . 1 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
hence <*2,1,3*> * <*3,2,1*> = <*3,1,2*> by A19, A28, A29, FINSEQ_1:62; :: thesis: verum

end;

thus <*3,2,1*> * <*2,1,3*> = <*2,3,1*> :: thesis: ( <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A30: hg . 1 = h . (g . 1) by A3, FUNCT_1:23
.= h . 2 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
A31: hg . 2 = h . (g . 2) by A3, FUNCT_1:23
.= h . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hg . 3 = h . (g . 3) by A3, FUNCT_1:23
.= h . 3 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hence <*3,2,1*> * <*2,1,3*> = <*2,3,1*> by A20, A30, A31, FINSEQ_1:62; :: thesis: verum

end;

thus <*3,2,1*> * <*3,2,1*> = <*1,2,3*> :: thesis: ( <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A32: hh . 1 = h . (h . 1) by A5, FUNCT_1:23
.= h . 3 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
A33: hh . 2 = h . (h . 2) by A5, FUNCT_1:23
.= h . 2 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
hh . 3 = h . (h . 3) by A5, FUNCT_1:23
.= h . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hence <*3,2,1*> * <*3,2,1*> = <*1,2,3*> by A21, A32, A33, FINSEQ_1:62; :: thesis: verum

end;

thus <*2,1,3*> * <*2,1,3*> = <*1,2,3*> :: thesis: ( <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A34: gg . 1 = g . (g . 1) by A3, FUNCT_1:23
.= g . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
A35: gg . 2 = g . (g . 2) by A3, FUNCT_1:23
.= g . 1 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
gg . 3 = g . (g . 3) by A3, FUNCT_1:23
.= g . 3 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hence <*2,1,3*> * <*2,1,3*> = <*1,2,3*> by A22, A34, A35, FINSEQ_1:62; :: thesis: verum

end;

thus <*1,3,2*> * <*1,3,2*> = <*1,2,3*> :: thesis: ( <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A36: ff . 1 = f . (f . 1) by A1, FUNCT_1:23
.= f . 1 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
A37: ff . 2 = f . (f . 2) by A1, FUNCT_1:23
.= f . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
ff . 3 = f . (f . 3) by A1, FUNCT_1:23
.= f . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hence <*1,3,2*> * <*1,3,2*> = <*1,2,3*> by A23, A36, A37, FINSEQ_1:62; :: thesis: verum

end;

thus <*1,3,2*> * <*2,3,1*> = <*3,2,1*> :: thesis: ( <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A38: fF . 1 = f . (F . 1) by A2, FUNCT_1:23
.= f . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
A39: fF . 2 = f . (F . 2) by A2, FUNCT_1:23
.= f . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
fF . 3 = f . (F . 3) by A2, FUNCT_1:23
.= f . 1 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hence <*1,3,2*> * <*2,3,1*> = <*3,2,1*> by A12, A38, A39, FINSEQ_1:62; :: thesis: verum

end;

thus <*2,3,1*> * <*2,3,1*> = <*3,1,2*> :: thesis: ( <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A40: FF . 1 = F . (F . 1) by A2, FUNCT_1:23
.= F . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
A41: FF . 2 = F . (F . 2) by A2, FUNCT_1:23
.= F . 3 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
FF . 3 = F . (F . 3) by A2, FUNCT_1:23
.= F . 1 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
hence <*2,3,1*> * <*2,3,1*> = <*3,1,2*> by A15, A40, A41, FINSEQ_1:62; :: thesis: verum

end;

thus <*2,3,1*> * <*3,1,2*> = <*1,2,3*> :: thesis: ( <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A42: FG . 1 = F . (G . 1) by A4, FUNCT_1:23
.= F . 3 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
A43: FG . 2 = F . (G . 2) by A4, FUNCT_1:23
.= F . 1 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
FG . 3 = F . (G . 3) by A4, FUNCT_1:23
.= F . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hence <*2,3,1*> * <*3,1,2*> = <*1,2,3*> by A16, A42, A43, FINSEQ_1:62; :: thesis: verum

end;

thus <*3,1,2*> * <*2,3,1*> = <*1,2,3*> :: thesis: ( <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A44: GF . 1 = G . (F . 1) by A2, FUNCT_1:23
.= G . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
A45: GF . 2 = G . (F . 2) by A2, FUNCT_1:23
.= G . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
GF . 3 = G . (F . 3) by A2, FUNCT_1:23
.= G . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
hence <*3,1,2*> * <*2,3,1*> = <*1,2,3*> by A17, A44, A45, FINSEQ_1:62; :: thesis: verum

end;

thus <*3,1,2*> * <*3,1,2*> = <*2,3,1*> :: thesis: ( <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )

proof

A46: GG . 1 = G . (G . 1) by A4, FUNCT_1:23
.= G . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
A47: GG . 2 = G . (G . 2) by A4, FUNCT_1:23
.= G . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
GG . 3 = G . (G . 3) by A4, FUNCT_1:23
.= G . 2 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hence <*3,1,2*> * <*3,1,2*> = <*2,3,1*> by A18, A46, A47, FINSEQ_1:62; :: thesis: verum

end;

thus <*1,3,2*> * <*3,2,1*> = <*2,3,1*> :: thesis: <*3,2,1*> * <*1,3,2*> = <*3,1,2*>

proof

A48: fh . 1 = f . (h . 1) by A5, FUNCT_1:23
.= f . 3 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
A49: fh . 2 = f . (h . 2) by A5, FUNCT_1:23
.= f . 2 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
fh . 3 = f . (h . 3) by A5, FUNCT_1:23
.= f . 1 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hence <*1,3,2*> * <*3,2,1*> = <*2,3,1*> by A13, A48, A49, FINSEQ_1:62; :: thesis: verum

end;

thus <*3,2,1*> * <*1,3,2*> = <*3,1,2*> :: thesis: verum

proof

A50: hf . 1 = h . (f . 1) by A1, FUNCT_1:23
.= h . 1 by FINSEQ_1:62
.= 3 by FINSEQ_1:62 ;
A51: hf . 2 = h . (f . 2) by A1, FUNCT_1:23
.= h . 3 by FINSEQ_1:62
.= 1 by FINSEQ_1:62 ;
hf . 3 = h . (f . 3) by A1, FUNCT_1:23
.= h . 2 by FINSEQ_1:62
.= 2 by FINSEQ_1:62 ;
hence <*3,2,1*> * <*1,3,2*> = <*3,1,2*> by A14, A50, A51, FINSEQ_1:62; :: thesis: verum

end;