set F = <*2,3,1*>;
set G = <*3,1,2*>;
set f = <*1,3,2*>;
set g = <*2,1,3*>;
set h = <*3,2,1*>;
A1: dom <*1,3,2*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then A2: 1 in dom <*1,3,2*> by ENUMSET1:def 1;
A3: <*1,3,2*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
A4: <*2,1,3*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
A5: 2 in dom <*1,3,2*> by A1, ENUMSET1:def 1;
A6: dom <*3,1,2*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then A7: 1 in dom <*3,1,2*> by ENUMSET1:def 1;
A8: 3 in dom <*3,1,2*> by A6, ENUMSET1:def 1;
A9: 2 in dom <*3,1,2*> by A6, ENUMSET1:def 1;
A10: 3 in dom <*1,3,2*> by A1, ENUMSET1:def 1;
A11: dom <*2,1,3*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then A12: 1 in dom <*2,1,3*> by ENUMSET1:def 1;
A13: 3 in dom <*2,1,3*> by A11, ENUMSET1:def 1;
A14: 2 in dom <*2,1,3*> by A11, ENUMSET1:def 1;
A15: dom <*3,2,1*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then A16: 1 in dom <*3,2,1*> by ENUMSET1:def 1;
A17: 3 in dom <*3,2,1*> by A15, ENUMSET1:def 1;
A18: 2 in dom <*3,2,1*> by A15, ENUMSET1:def 1;
A19: <*1,3,2*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
A20: <*3,1,2*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
A21: dom <*2,3,1*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then A22: 1 in dom <*2,3,1*> by ENUMSET1:def 1;
A23: 3 in dom <*2,3,1*> by A21, ENUMSET1:def 1;
A24: 2 in dom <*2,3,1*> by A21, ENUMSET1:def 1;
A25: <*3,2,1*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
A26: <*2,3,1*> is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then 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 A4, A25, A20, A19, Th36;
A27: 3 = len g by FINSEQ_1:45;
then reconsider gf = g * f as FinSequence of Seg 3 by A3, FINSEQ_2:46;
A28: gf . 1 = g . (f . 1) by A2, FUNCT_1:13
.= g . 1
.= 2 ;
A29: g is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then reconsider gg = g * g as FinSequence of Seg 3 by A27, FINSEQ_2:46;
A30: gg . 1 = g . (g . 1) by A12, FUNCT_1:13
.= g . 2
.= 1 ;
A31: 3 = len f by FINSEQ_1:45;
then reconsider fg = f * g as FinSequence of Seg 3 by A4, FINSEQ_2:46;
A32: fg . 2 = f . (g . 2) by A14, FUNCT_1:13
.= f . 1
.= 1 ;
A33: gf . 3 = g . (f . 3) by A10, FUNCT_1:13
.= g . 2
.= 1 ;
A34: gf . 2 = g . (f . 2) by A5, FUNCT_1:13
.= g . 3
.= 3 ;
A35: f is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then reconsider ff = f * f as FinSequence of Seg 3 by A31, FINSEQ_2:46;
len gf = 3 by A27, A35, FINSEQ_2:43;
hence <*2,1,3*> * <*1,3,2*> = <*2,3,1*> by A28, A34, A33, FINSEQ_1:45; :: 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*> )
A36: fg . 1 = f . (g . 1) by A12, FUNCT_1:13
.= f . 2
.= 3 ;
A37: fg . 3 = f . (g . 3) by A13, FUNCT_1:13
.= f . 3
.= 2 ;
len fg = 3 by A31, A29, FINSEQ_2:43;
hence <*1,3,2*> * <*2,1,3*> = <*3,1,2*> by A36, A32, A37, FINSEQ_1:45; :: 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*> )
A38: ff . 2 = f . (f . 2) by A5, FUNCT_1:13
.= f . 3
.= 2 ;
A39: gg . 3 = g . (g . 3) by A13, FUNCT_1:13
.= g . 3
.= 3 ;
A40: gg . 2 = g . (g . 2) by A14, FUNCT_1:13
.= g . 1
.= 2 ;
A41: h is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then reconsider gh = g * h as FinSequence of Seg 3 by A27, FINSEQ_2:46;
A42: gh . 1 = g . (h . 1) by A16, FUNCT_1:13
.= g . 3
.= 3 ;
A43: gh . 3 = g . (h . 3) by A17, FUNCT_1:13
.= g . 1
.= 2 ;
A44: gh . 2 = g . (h . 2) by A18, FUNCT_1:13
.= g . 2
.= 1 ;
A45: 3 = len h by FINSEQ_1:45;
then reconsider hf = h * f as FinSequence of Seg 3 by A19, FINSEQ_2:46;
reconsider hh = h * h as FinSequence of Seg 3 by A45, A41, FINSEQ_2:46;
A46: hh . 1 = h . (h . 1) by A16, FUNCT_1:13
.= h . 3
.= 1 ;
reconsider fh = f * h as FinSequence of Seg 3 by A25, A31, FINSEQ_2:46;
A47: fh . 1 = f . (h . 1) by A16, FUNCT_1:13
.= f . 3
.= 2 ;
A48: fh . 3 = f . (h . 3) by A17, FUNCT_1:13
.= f . 1
.= 1 ;
reconsider fF = f * F as FinSequence of Seg 3 by A26, A31, FINSEQ_2:46;
A49: fF . 1 = f . (F . 1) by A22, FUNCT_1:13
.= f . 2
.= 3 ;
A50: fF . 2 = f . (F . 2) by A24, FUNCT_1:13
.= f . 3
.= 2 ;
reconsider hg = h * g as FinSequence of Seg 3 by A45, A29, FINSEQ_2:46;
A51: hg . 1 = h . (g . 1) by A12, FUNCT_1:13
.= h . 2
.= 2 ;
A52: hg . 2 = h . (g . 2) by A14, FUNCT_1:13
.= h . 1
.= 3 ;
A53: hh . 3 = h . (h . 3) by A17, FUNCT_1:13
.= h . 1
.= 3 ;
A54: hh . 2 = h . (h . 2) by A18, FUNCT_1:13
.= h . 2
.= 2 ;
len gh = 3 by A27, A41, FINSEQ_2:43;
hence <*2,1,3*> * <*3,2,1*> = <*3,1,2*> by A42, A44, A43, FINSEQ_1:45; :: 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*> )
A55: ff . 3 = f . (f . 3) by A10, FUNCT_1:13
.= f . 2
.= 3 ;
A56: hg . 3 = h . (g . 3) by A13, FUNCT_1:13
.= h . 3
.= 1 ;
len hg = 3 by A45, A29, FINSEQ_2:43;
hence <*3,2,1*> * <*2,1,3*> = <*2,3,1*> by A51, A52, A56, FINSEQ_1:45; :: 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*> )
len hh = 3 by A45, A41, FINSEQ_2:43;
hence <*3,2,1*> * <*3,2,1*> = <*1,2,3*> by A46, A54, A53, FINSEQ_1:45; :: 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*> )
len gg = 3 by A27, A29, FINSEQ_2:43;
hence <*2,1,3*> * <*2,1,3*> = <*1,2,3*> by A30, A40, A39, FINSEQ_1:45; :: 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*> )
A57: ff . 1 = f . (f . 1) by A2, FUNCT_1:13
.= f . 1
.= 1 ;
A58: fF . 3 = f . (F . 3) by A23, FUNCT_1:13
.= f . 1
.= 1 ;
len ff = 3 by A31, A35, FINSEQ_2:43;
hence <*1,3,2*> * <*1,3,2*> = <*1,2,3*> by A57, A38, A55, FINSEQ_1:45; :: 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*> )
A59: F is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then len fF = 3 by A31, FINSEQ_2:43;
hence <*1,3,2*> * <*2,3,1*> = <*3,2,1*> by A49, A50, A58, FINSEQ_1:45; :: 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*> )
A60: fh . 2 = f . (h . 2) by A18, FUNCT_1:13
.= f . 2
.= 3 ;
A61: 3 = len F by FINSEQ_1:45;
then reconsider FF = F * F as FinSequence of Seg 3 by A26, FINSEQ_2:46;
reconsider FG = F * G as FinSequence of Seg 3 by A20, A61, FINSEQ_2:46;
A62: FG . 1 = F . (G . 1) by A7, FUNCT_1:13
.= F . 3
.= 1 ;
A63: FG . 2 = F . (G . 2) by A9, FUNCT_1:13
.= F . 1
.= 2 ;
A64: FF . 3 = F . (F . 3) by A23, FUNCT_1:13
.= F . 1
.= 2 ;
A65: FG . 3 = F . (G . 3) by A8, FUNCT_1:13
.= F . 2
.= 3 ;
A66: FF . 2 = F . (F . 2) by A24, FUNCT_1:13
.= F . 3
.= 1 ;
A67: FF . 1 = F . (F . 1) by A22, FUNCT_1:13
.= F . 2
.= 3 ;
A68: 3 = len G by FINSEQ_1:45;
then reconsider GF = G * F as FinSequence of Seg 3 by A26, FINSEQ_2:46;
reconsider GG = G * G as FinSequence of Seg 3 by A20, A68, FINSEQ_2:46;
A69: GG . 1 = G . (G . 1) by A7, FUNCT_1:13
.= G . 3
.= 2 ;
A70: GG . 2 = G . (G . 2) by A9, FUNCT_1:13
.= G . 1
.= 3 ;
A71: GF . 3 = G . (F . 3) by A23, FUNCT_1:13
.= G . 1
.= 3 ;
A72: GG . 3 = G . (G . 3) by A8, FUNCT_1:13
.= G . 2
.= 1 ;
A73: GF . 2 = G . (F . 2) by A24, FUNCT_1:13
.= G . 3
.= 2 ;
A74: GF . 1 = G . (F . 1) by A22, FUNCT_1:13
.= G . 2
.= 1 ;
len FF = 3 by A61, A59, FINSEQ_2:43;
hence <*2,3,1*> * <*2,3,1*> = <*3,1,2*> by A67, A66, A64, FINSEQ_1:45; :: 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*> )
A75: G is Permutation of (Seg 3) by Th27, MATRIX_1:def 12;
then len FG = 3 by A61, FINSEQ_2:43;
hence <*2,3,1*> * <*3,1,2*> = <*1,2,3*> by A62, A63, A65, FINSEQ_1:45; :: 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*> )
A76: hf . 3 = h . (f . 3) by A10, FUNCT_1:13
.= h . 2
.= 2 ;
len GF = 3 by A68, A59, FINSEQ_2:43;
hence <*3,1,2*> * <*2,3,1*> = <*1,2,3*> by A74, A73, A71, FINSEQ_1:45; :: 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*> )
len GG = 3 by A68, A75, FINSEQ_2:43;
hence <*3,1,2*> * <*3,1,2*> = <*2,3,1*> by A69, A70, A72, FINSEQ_1:45; :: thesis: ( <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A77: hf . 2 = h . (f . 2) by A5, FUNCT_1:13
.= h . 3
.= 1 ;
len fh = 3 by A31, A41, FINSEQ_2:43;
hence <*1,3,2*> * <*3,2,1*> = <*2,3,1*> by A47, A60, A48, FINSEQ_1:45; :: thesis: <*3,2,1*> * <*1,3,2*> = <*3,1,2*>
A78: hf . 1 = h . (f . 1) by A2, FUNCT_1:13
.= h . 1
.= 3 ;
len hf = 3 by A45, A35, FINSEQ_2:43;
hence <*3,2,1*> * <*1,3,2*> = <*3,1,2*> by A78, A77, A76, FINSEQ_1:45; :: thesis: verum