let D be non empty set ; :: thesis:
let F, G be FinSequence of D; :: thesis:
let g be BinOp of D; :: thesis:
assume that
A1: g is associative and
A2: g is commutative ; :: thesis:
defpred S₁[ Nat] means for H1, H2 being FinSequence of D st len H1 >= 1 & len H1 = $1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2;

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

let H1, H2 be FinSequence of D; :: thesis:
assume that
len H1 >= 1 and
A5: len H1 = k + 1 and
A6: len H1 = len H2 ; :: thesis:
reconsider p = H2 | (Seg k) as FinSequence of D by FINSEQ_1:18;
let f be Permutation of (dom H1); :: thesis:
A7: dom H1 = Seg (k + 1) by A5, FINSEQ_1:def 3;
then A8: rng f = Seg (k + 1) by FUNCT_2:def 3;

A9: now :: thesis:

let n be Nat; :: thesis:
assume n in dom f ; :: thesis:
then f . n in Seg (k + 1) by A8, FUNCT_1:def 3;
hence f . n is Element of NAT ; :: thesis:

end;

A10: rng H2 c= D by FINSEQ_1:def 4;
A11: dom f = Seg (k + 1) by A7, FUNCT_2:def 1;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A13: f . (k + 1) in Seg (k + 1) by A11, A8, FUNCT_1:def 3;
then reconsider n = f . (k + 1) as Element of NAT ;
A14: dom H2 = Seg (k + 1) by A5, A6, FINSEQ_1:def 3;
then H2 . (k + 1) in rng H2 by A12, FUNCT_1:def 3;
then reconsider d = H2 . (k + 1) as Element of D by A10;
A15: n <= k + 1 by A13, FINSEQ_1:1;
then consider m2 being Nat such that
A16: n + m2 = k + 1 by NAT_1:10;
defpred S₂[ Nat, object ] means $2 = H1 . (n + $1);
1 <= n by A13, FINSEQ_1:1;
then consider m1 being Nat such that
A17: 1 + m1 = n by NAT_1:10;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def 12;
A18: for j being Nat st j in Seg m2 holds
ex x being object st S₂[j,x] ;
consider q2 being FinSequence such that
A19: dom q2 = Seg m2 and
A20: for k being Nat st k in Seg m2 holds
S₂[k,q2 . k] from FINSEQ_1:sch 1(A18);
rng q2 c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng q2 ; :: thesis:
then consider y being object such that
A21: y in findom q2 and
A22: x = q2 . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A21, SETWISEO:9;
1 <= y by A19, A21, FINSEQ_1:1;
then A23: 1 <= n + y by NAT_1:12;
y <= m2 by A19, A21, FINSEQ_1:1;
then n + y <= len H1 by A5, A16, XREAL_1:7;
then n + y in Seg (len H1) by A23, FINSEQ_1:1;
then n + y in dom H1 by FINSEQ_1:def 3;
then A24: H1 . (n + y) in rng H1 by FUNCT_1:def 3;
rng H1 c= D by FINSEQ_1:def 4;
then reconsider xx = H1 . (n + y) as Element of D by A24;
xx in D ;
hence x in D by A19, A20, A21, A22; :: thesis:

end;

then reconsider q2 = q2 as FinSequence of D by FINSEQ_1:def 4;
reconsider q1 = H1 | (Seg m1) as FinSequence of D by FINSEQ_1:18;
defpred S₃[ Nat, object ] means ( ( f . $1 in dom q1 implies $2 = f . $1 ) & ( not f . $1 in dom q1 implies for l being Nat st l = f . $1 holds
$2 = l - 1 ) );
A25: k <= k + 1 by NAT_1:12;
then A26: Seg k c= Seg (k + 1) by FINSEQ_1:5;
A27: for i being Nat st i in Seg k holds
ex y being object st S₃[i,y]

proof

let i be Nat; :: thesis:
assume A28: i in Seg k ; :: thesis:

now :: thesis:

f . i in Seg (k + 1) by A11, A8, A26, A28, FUNCT_1:def 3;
then reconsider j = f . i as Element of NAT ;
assume A29: not f . i in dom q1 ; :: thesis:
take y = j - 1; :: thesis:
thus ( f . i in dom q1 implies y = f . i ) by A29; :: thesis:
assume not f . i in dom q1 ; :: thesis:
let t be Nat; :: thesis:
assume t = f . i ; :: thesis:
hence y = t - 1 ; :: thesis:

end;

hence ex y being object st S₃[i,y] ; :: thesis:

end;

consider gg being FinSequence such that
A30: dom gg = Seg k and
A31: for i being Nat st i in Seg k holds
S₃[i,gg . i] from FINSEQ_1:sch 1(A27);
A32: dom p = Seg k by A5, A6, A25, FINSEQ_1:17;
m1 <= n by A17, NAT_1:11;
then A33: m1 <= k + 1 by A15, XXREAL_0:2;
then A34: dom q1 = Seg m1 by A5, FINSEQ_1:17;

A35: now :: thesis:

let i, l be Nat; :: thesis:
assume that
A36: l = f . i and
A37: not f . i in dom q1 and
A38: i in dom gg ; :: thesis:
A39: ( l < 1 or m1 < l ) by A34, A36, A37, FINSEQ_1:1;

A40: now :: thesis:

assume m1 + 1 = l ; :: thesis:
then k + 1 = i by A12, A11, A17, A26, A30, A36, A38, FUNCT_1:def 4;
then k + 1 <= k + 0 by A30, A38, FINSEQ_1:1;
hence contradiction by XREAL_1:6; :: thesis:

end;

f . i in rng f by A11, A26, A30, A38, FUNCT_1:def 3;
then m1 + 1 <= l by A8, A36, A39, FINSEQ_1:1, NAT_1:13;
then m1 + 1 < l by A40, XXREAL_0:1;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; :: thesis:

end;

1 + k = 1 + (m1 + m2) by A17, A16;
then A41: m1 <= k by NAT_1:11;
A42: rng gg c= dom p

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng gg ; :: thesis:
then consider x being object such that
A43: x in findom gg and
A44: gg . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A43, SETWISEO:9;

now :: thesis:

per cases ;

suppose A45: f . x in dom q1 ; :: thesis:

A46: dom q1 c= dom p by A41, A34, A32, FINSEQ_1:5;
f . x = gg . x by A30, A31, A43, A45;
hence y in dom p by A44, A45, A46; :: thesis:

end;

suppose A47: not f . x in dom q1 ; :: thesis:

reconsider j = f . x as Element of NAT by A11, A26, A9, A30, A43;
A48: f . x in Seg (k + 1) by A11, A8, A26, A30, A43, FUNCT_1:def 3;
( j < 1 or m1 < j ) by A34, A47, FINSEQ_1:1;
then reconsider l = j - 1 as Element of NAT by A48, FINSEQ_1:1, NAT_1:20;
j <= k + 1 by A48, FINSEQ_1:1;
then A49: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by A35, A43, A47;
then A50: (m1 + 2) - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then A51: 1 <= l by A50, XXREAL_0:2;
gg . x = j - 1 by A30, A31, A43, A47;
hence y in dom p by A32, A44, A51, A49, FINSEQ_1:1; :: thesis:

end;

hence y in dom p ; :: thesis:

end;

A52: len q1 = m1 by A5, A33, FINSEQ_1:17;

A53: now :: thesis:

let j be Nat; :: thesis:
assume A54: j in dom q2 ; :: thesis:
len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22
.= n by A17, FINSEQ_1:39 ;
hence H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j by A19, A20, A54; :: thesis:

end;

set q = q1 ^ q2;
A55: len q2 = m2 by A19, FINSEQ_1:def 3;
then A56: len (q1 ^ q2) = m1 + m2 by A52, FINSEQ_1:22;
then A57: dom (q1 ^ q2) = Seg k by A17, A16, FINSEQ_1:def 3;
then reconsider gg = gg as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A32, A30, A42, FUNCT_2:2;
A58: len p = k by A5, A6, A25, FINSEQ_1:17;
A59: rng gg = dom (q1 ^ q2)

proof

thus rng gg c= dom (q1 ^ q2) by A17, A16, A56, A32, A42, FINSEQ_1:def 3; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A60: y in dom (q1 ^ q2) ; :: thesis:
then reconsider j = y as Element of NAT ;
consider x being object such that
A61: x in dom f and
A62: f . x = y by A8, A26, A57, A60, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A11, A61;

now :: thesis:

per cases ;

suppose A63: x in dom gg ; :: thesis:

now :: thesis:

per cases ;

suppose f . x in dom q1 ; :: thesis:

then gg . x = f . x by A30, A31, A63;
hence y in rng gg by A62, A63, FUNCT_1:def 3; :: thesis:

end;

suppose A64: not f . x in dom q1 ; :: thesis:

j <= k by A57, A60, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A8, FINSEQ_1:1;
then consider x1 being object such that
A65: x1 in dom f and
A66: f . x1 = j + 1 by FUNCT_1:def 3;

A67: now :: thesis:

assume not x1 in dom gg ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A65, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then A68: j + 1 = m1 + 1 by A17, A66, TARSKI:def 1;
1 <= j by A57, A60, FINSEQ_1:1;
hence contradiction by A34, A62, A64, A68, FINSEQ_1:1; :: thesis:

end;

( j < 1 or m1 < j ) by A34, A62, A64, FINSEQ_1:1;
then not j + 1 <= m1 by A57, A60, FINSEQ_1:1, NAT_1:13;
then not f . x1 in dom q1 by A34, A66, FINSEQ_1:1;
then gg . x1 = (j + 1) - 1 by A30, A31, A66, A67
.= y ;
hence y in rng gg by A67, FUNCT_1:def 3; :: thesis:

end;

hence y in rng gg ; :: thesis:

end;

suppose A69: not x in dom gg ; :: thesis:

j <= k by A57, A60, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A8, FINSEQ_1:1;
then consider x1 being object such that
A70: x1 in dom f and
A71: f . x1 = j + 1 by FUNCT_1:def 3;
x in (Seg (k + 1)) \ (Seg k) by A7, A30, A61, A69, XBOOLE_0:def 5;
then x in {(k + 1)} by FINSEQ_3:15;
then A72: x = k + 1 by TARSKI:def 1;

A73: now :: thesis:

assume not x1 in dom gg ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A70, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then j + 1 = j + 0 by A62, A72, A71, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

m1 <= j by A17, A62, A72, XREAL_1:29;
then not j + 1 <= m1 by NAT_1:13;
then not f . x1 in dom q1 by A34, A71, FINSEQ_1:1;
then gg . x1 = (j + 1) - 1 by A30, A31, A71, A73
.= y ;
hence y in rng gg by A73, FUNCT_1:def 3; :: thesis:

end;

hence y in rng gg ; :: thesis:

end;

assume A74: for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ; :: thesis:
then A75: H2 . (k + 1) = H1 . (f . (k + 1)) by A14, FINSEQ_1:4;

A76: now :: thesis:

let j be Nat; :: thesis:
assume A77: j in dom (q1 ^ <*d*>) ; :: thesis:

A78: now :: thesis:

assume j in Seg m1 ; :: thesis:
then A79: j in dom q1 by A5, A33, FINSEQ_1:17;
then q1 . j = H1 . j by FUNCT_1:47;
hence H1 . j = (q1 ^ <*d*>) . j by A79, FINSEQ_1:def 7; :: thesis:

end;

A80: now :: thesis:

( 1 in Seg 1 & len <*d*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39;
then 1 in dom <*d*> by FINSEQ_1:def 3;
then A81: (q1 ^ <*d*>) . ((len q1) + 1) = <*d*> . 1 by FINSEQ_1:def 7;
assume j in {n} ; :: thesis:
then j = n by TARSKI:def 1;
hence (q1 ^ <*d*>) . j = H1 . j by A75, A17, A52, A81; :: thesis:

end;

len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40 ;
then j in Seg (m1 + 1) by A77, FINSEQ_1:def 3;
then j in (Seg m1) \/ {n} by A17, FINSEQ_1:9;
hence H1 . j = (q1 ^ <*d*>) . j by A78, A80, XBOOLE_0:def 3; :: thesis:

end;

gg is one-to-one

proof

let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A82: y1 in dom gg and
A83: y2 in dom gg and
A84: gg . y1 = gg . y2 ; :: thesis:
reconsider j1 = y1, j2 = y2 as Element of NAT by A30, A82, A83;
A85: f . y2 in Seg (k + 1) by A11, A8, A26, A30, A83, FUNCT_1:def 3;
A86: f . y1 in Seg (k + 1) by A11, A8, A26, A30, A82, FUNCT_1:def 3;
then reconsider a = f . y1, b = f . y2 as Element of NAT by A85;

now :: thesis:

per cases ;

suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis:

then ( gg . j1 = f . y1 & gg . j2 = f . y2 ) by A30, A31, A82, A83;
hence y1 = y2 by A11, A26, A30, A82, A83, A84, FUNCT_1:def 4; :: thesis:

end;

suppose A87: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis:

then A88: a <= m1 by A34, FINSEQ_1:1;
( gg . j1 = a & gg . j2 = b - 1 ) by A30, A31, A82, A83, A87;
then A89: (b - 1) + 1 <= m1 + 1 by A84, A88, XREAL_1:6;
1 <= b by A85, FINSEQ_1:1;
then A90: b in Seg (m1 + 1) by A89, FINSEQ_1:1;
not b in Seg m1 by A5, A33, A87, FINSEQ_1:17;
then b in (Seg (m1 + 1)) \ (Seg m1) by A90, XBOOLE_0:def 5;
then b in {(m1 + 1)} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by A12, A11, A17, A26, A30, A83, FUNCT_1:def 4;
hence y1 = y2 by A30, A83, FINSEQ_3:8; :: thesis:

end;

suppose A91: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis:

then A92: b <= m1 by A34, FINSEQ_1:1;
( gg . j1 = a - 1 & gg . j2 = b ) by A30, A31, A82, A83, A91;
then A93: (a - 1) + 1 <= m1 + 1 by A84, A92, XREAL_1:6;
1 <= a by A86, FINSEQ_1:1;
then A94: a in Seg (m1 + 1) by A93, FINSEQ_1:1;
not a in Seg m1 by A5, A33, A91, FINSEQ_1:17;
then a in (Seg (m1 + 1)) \ (Seg m1) by A94, XBOOLE_0:def 5;
then a in {(m1 + 1)} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by A12, A11, A17, A26, A30, A82, FUNCT_1:def 4;
hence y1 = y2 by A30, A82, FINSEQ_3:8; :: thesis:

end;

suppose A95: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis:

then gg . j2 = b - 1 by A30, A31, A83;
then A96: gg . y2 = b + (- 1) ;
gg . j1 = a - 1 by A30, A31, A82, A95;
then gg . j1 = a + (- 1) ;
then a = b by A84, A96, XCMPLX_1:2;
hence y1 = y2 by A11, A26, A30, A82, A83, FUNCT_1:def 4; :: thesis:

end;

hence y1 = y2 ; :: thesis:

end;

then reconsider gg = gg as Permutation of (dom (q1 ^ q2)) by A59, FUNCT_2:57;
(len (q1 ^ <*d*>)) + (len q2) = ((len q1) + (len <*d*>)) + m2 by A55, FINSEQ_1:22
.= k + 1 by A17, A16, A52, FINSEQ_1:40 ;
then dom H1 = Seg ((len (q1 ^ <*d*>)) + (len q2)) by A5, FINSEQ_1:def 3;
then A97: H1 = (q1 ^ <*d*>) ^ q2 by A76, A53, FINSEQ_1:def 7;

A98: now :: thesis:

let i be Nat; :: thesis:
assume A99: i in dom p ; :: thesis:
then f . i in rng f by A11, A26, A32, FUNCT_1:def 3;
then reconsider j = f . i as Element of NAT by A8;

now :: thesis:

per cases ;

suppose A100: f . i in dom q1 ; :: thesis:

then A101: ( f . i = gg . i & H1 . j = q1 . j ) by A32, A31, A99, FUNCT_1:47;
( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47;
hence p . i = (q1 ^ q2) . (gg . i) by A100, A101, FINSEQ_1:def 7; :: thesis:

end;

suppose A102: not f . i in dom q1 ; :: thesis:

then m1 + 2 <= j by A32, A30, A35, A99;
then A103: (m1 + 2) - 1 <= j - 1 by XREAL_1:9;
m1 < m1 + 1 by XREAL_1:29;
then A104: m1 < j - 1 by A103, XXREAL_0:2;
then m1 < j by XREAL_1:146, XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A105: not j1 in dom q1 by A34, A104, FINSEQ_1:1;
A106: gg . i = j - 1 by A32, A31, A99, A102;
then j - 1 in dom (q1 ^ q2) by A32, A30, A59, A99, FUNCT_1:def 3;
then consider a being Nat such that
A107: a in dom q2 and
A108: j1 = (len q1) + a by A105, FINSEQ_1:25;
A109: len <*d*> = 1 by FINSEQ_1:39;
A110: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47;
A111: H1 = q1 ^ (<*d*> ^ q2) by A97, FINSEQ_1:32;
j in dom H1 by A7, A11, A8, A26, A32, A99, FUNCT_1:def 3;
then consider b being Nat such that
A112: b in dom (<*d*> ^ q2) and
A113: j = (len q1) + b by A102, A111, FINSEQ_1:25;
A114: H1 . j = (<*d*> ^ q2) . b by A111, A112, A113, FINSEQ_1:def 7;
A115: b = 1 + a by A108, A113;
(q1 ^ q2) . (j - 1) = q2 . a by A107, A108, FINSEQ_1:def 7;
hence p . i = (q1 ^ q2) . (gg . i) by A106, A110, A107, A114, A115, A109, FINSEQ_1:def 7; :: thesis:

end;

hence p . i = (q1 ^ q2) . (gg . i) ; :: thesis:

end;

now :: thesis:

per cases ;

suppose A116: len p <> 0 ; :: thesis:

A117: H2 = p ^ <*d*> by A5, A6, FINSEQ_3:55;
g "**" p = g "**" (q1 ^ q2) by A4, A17, A16, A58, A56, A98, A116, NAT_1:14;
then A118: g "**" H2 = g . ((g "**" (q1 ^ q2)),d) by A116, A117, Th4, NAT_1:14;

now :: thesis:

per cases ;

suppose A119: ( len q1 <> 0 & len q2 <> 0 ) ; :: thesis:

( len (<*d*> ^ q2) = (len <*d*>) + (len q2) & len <*d*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
then A120: len (<*d*> ^ q2) >= 1 by NAT_1:12;
A121: len q1 >= 1 by A119, NAT_1:14;
len q2 >= 1 by A119, NAT_1:14;
then g "**" H2 = g . ((g . ((g "**" q1),(g "**" q2))),d) by A1, A118, A121, Th5
.= g . ((g "**" q1),(g . ((g "**" q2),d))) by A1, BINOP_1:def 3
.= g . ((g "**" q1),(g . (d,(g "**" q2)))) by A2, BINOP_1:def 2
.= g . ((g "**" q1),(g "**" (<*d*> ^ q2))) by A1, A119, Th6, NAT_1:14
.= g "**" (q1 ^ (<*d*> ^ q2)) by A1, A121, A120, Th5
.= g "**" H1 by A97, FINSEQ_1:32 ;
hence g "**" H1 = g "**" H2 ; :: thesis:

end;

suppose ( len q1 = 0 & len q2 <> 0 ) ; :: thesis:

then A122: q1 = {} ;
then A123: H1 = <*d*> ^ q2 by A97, FINSEQ_1:34
.= <*d*> ^ (q1 ^ q2) by A122, FINSEQ_1:34 ;
g "**" H2 = g . (d,(g "**" (q1 ^ q2))) by A2, A118, BINOP_1:def 2
.= g "**" (<*d*> ^ (q1 ^ q2)) by A1, A17, A16, A58, A56, A116, Th6, NAT_1:14 ;
hence g "**" H1 = g "**" H2 by A123; :: thesis:

end;

suppose ( len q1 <> 0 & len q2 = 0 ) ; :: thesis:

then A124: q2 = {} ;
then H1 = q1 ^ <*d*> by A97, FINSEQ_1:34
.= (q1 ^ q2) ^ <*d*> by A124, FINSEQ_1:34 ;
hence g "**" H1 = g "**" H2 by A17, A16, A58, A56, A116, A118, Th4, NAT_1:14; :: thesis:

end;

suppose ( len q1 = 0 & len q2 = 0 ) ; :: thesis:

then len (q1 ^ q2) = 0 + 0 by FINSEQ_1:22;
hence g "**" H1 = g "**" H2 by A6, A17, A16, A56, A116, FINSEQ_1:17; :: thesis:

end;

hence g "**" H1 = g "**" H2 ; :: thesis:

end;

suppose A125: len p = 0 ; :: thesis:

then dom H1 = {1} by A5, A58, FINSEQ_1:2, FINSEQ_1:def 3;
then A126: ( dom f = {1} & rng f = {1} ) by FUNCT_2:def 1, FUNCT_2:def 3;
1 in {1} by TARSKI:def 1;
then f . 1 in {1} by A126, FUNCT_1:def 3;
then H1 . 1 = H2 . 1 by A75, A58, A125, TARSKI:def 1;
then H1 = <*d*> by A5, A58, A125, FINSEQ_1:40;
hence g "**" H1 = g "**" H2 by A5, A6, A58, A125, FINSEQ_1:40; :: thesis:

end;

hence g "**" H1 = g "**" H2 ; :: thesis:

end;

let f be Permutation of (dom F); :: thesis:
A127: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A127, A3);
hence ( len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G ) ; :: thesis: