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