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:
let f be Permutation of (dom F); :: thesis:
defpred S₁[ Element of 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 Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2;
A3: S₁[ 0 ] ;

A4: now

let k be Element of NAT ; :: thesis:
assume A5: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let H1, H2 be FinSequence of D; :: thesis:
assume that
len H1 >= 1 and
A6: len H1 = k + 1 and
A7: len H1 = len H2 ; :: thesis:
let f be Permutation of (dom H1); :: thesis:
assume A8: for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ; :: thesis:
reconsider p = H2 | (Seg k) as FinSequence of D by FINSEQ_1:23;
A9: k + 1 in Seg (k + 1) by FINSEQ_1:6;
A10: ( dom H2 = Seg (k + 1) & dom H1 = Seg (k + 1) ) by A6, A7, FINSEQ_1:def 3;
( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ;
then A11: ( dom f = Seg (k + 1) & rng f = Seg (k + 1) ) by A10, FUNCT_2:def 1, FUNCT_2:def 3;
then A12: f . (k + 1) in Seg (k + 1) by A9, FUNCT_1:def 5;
then reconsider n = f . (k + 1) as Element of NAT ;
A13: H2 . (k + 1) = H1 . (f . (k + 1)) by A8, A10, FINSEQ_1:6;
( H2 . (k + 1) in rng H2 & rng H2 c= D ) by A9, A10, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider d = H2 . (k + 1) as Element of D ;
1 <= n by A12, FINSEQ_1:3;
then consider m1 being Nat such that
A14: 1 + m1 = n by NAT_1:10;
A15: n <= k + 1 by A12, FINSEQ_1:3;
then consider m2 being Nat such that
A16: n + m2 = k + 1 by NAT_1:10;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def 13;
reconsider q1 = H1 | (Seg m1) as FinSequence of D by FINSEQ_1:23;
defpred S₂[ Nat, set ] means $2 = H1 . (n + $1);
A18: for j being Nat st j in Seg m2 holds
ex x being set 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 set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng q2 ; :: thesis:
then consider y being set such that
A21: y in findom q2 and
A22: x = q2 . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A21, SETWISEO:14;
( 1 <= y & y <= n + y ) by A19, A21, FINSEQ_1:3, NAT_1:12;
then A23: 1 <= n + y by XXREAL_0:2;
y <= m2 by A19, A21, FINSEQ_1:3;
then n + y <= len H1 by A6, A16, XREAL_1:9;
then n + y in Seg (len H1) by A23, FINSEQ_1:3;
then n + y in dom H1 by FINSEQ_1:def 3;
then ( H1 . (n + y) in rng H1 & rng H1 c= D ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider xx = H1 . (n + y) as Element of D ;
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;
set q = q1 ^ q2;
A24: k <= k + 1 by NAT_1:12;
then A25: len p = k by A6, A7, FINSEQ_1:21;
m1 <= n by A14, NAT_1:11;
then A26: m1 <= k + 1 by A15, XXREAL_0:2;
then A27: ( len q1 = m1 & len q2 = m2 ) by A6, A19, FINSEQ_1:21, FINSEQ_1:def 3;
then A28: len (q1 ^ q2) = m1 + m2 by FINSEQ_1:35;
A29: 1 + k = 1 + (m1 + m2) by A14, A16;
(len (q1 ^ <*d*>)) + (len q2) = ((len q1) + (len <*d*>)) + m2 by A27, FINSEQ_1:35
.= k + 1 by A14, A16, A27, FINSEQ_1:57 ;
then A30: dom H1 = Seg ((len (q1 ^ <*d*>)) + (len q2)) by A6, FINSEQ_1:def 3;

A31: now

let j be Nat; :: thesis:
assume A32: j in dom (q1 ^ <*d*>) ; :: thesis:
len (q1 ^ <*d*>) = m1 + (len <*d*>) by A27, FINSEQ_1:35
.= m1 + 1 by FINSEQ_1:57 ;
then j in Seg (m1 + 1) by A32, FINSEQ_1:def 3;
then A33: j in (Seg m1) \/ {n} by A14, FINSEQ_1:11;

A34: now

assume j in Seg m1 ; :: thesis:
then A35: j in dom q1 by A6, A26, FINSEQ_1:21;
then q1 . j = H1 . j by FUNCT_1:70;
hence H1 . j = (q1 ^ <*d*>) . j by A35, FINSEQ_1:def 7; :: thesis:

end;

now

assume j in {n} ; :: thesis:
then A36: j = n by TARSKI:def 1;
( 1 in Seg 1 & len <*d*> = 1 ) by FINSEQ_1:3, FINSEQ_1:56;
then 1 in dom <*d*> by FINSEQ_1:def 3;
then (q1 ^ <*d*>) . ((len q1) + 1) = <*d*> . 1 by FINSEQ_1:def 7;
hence (q1 ^ <*d*>) . j = H1 . j by A13, A14, A27, A36, FINSEQ_1:57; :: thesis:

end;

hence H1 . j = (q1 ^ <*d*>) . j by A33, A34, XBOOLE_0:def 3; :: thesis:

end;

now

let j be Nat; :: thesis:
assume A37: j in dom q2 ; :: thesis:
len (q1 ^ <*d*>) = m1 + (len <*d*>) by A27, FINSEQ_1:35
.= n by A14, FINSEQ_1:56 ;
hence H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j by A19, A20, A37; :: thesis:

end;

then A38: H1 = (q1 ^ <*d*>) ^ q2 by A30, A31, FINSEQ_1:def 7;
A39: m1 <= k by A29, NAT_1:11;
A40: Seg k c= Seg (k + 1) by A24, FINSEQ_1:7;

A41: now

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

end;

A42: dom q1 = Seg m1 by A6, A26, FINSEQ_1:21;
A43: ( dom p = Seg k & dom (q1 ^ q2) = Seg k ) by A6, A7, A14, A16, A24, A28, FINSEQ_1:21, FINSEQ_1:def 3;
defpred S₃[ Nat, set ] means ( ( f . $1 in dom q1 implies $2 = f . $1 ) & ( not f . $1 in dom q1 implies for l being Element of NAT st l = f . $1 holds
$2 = l - 1 ) );
A44: for i being Nat st i in Seg k holds
ex y being set st S₃[i,y]

proof

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

now

assume A46: not f . i in dom q1 ; :: thesis:
f . i in Seg (k + 1) by A11, A40, A45, FUNCT_1:def 5;
then reconsider j = f . i as Element of NAT ;
take y = j - 1; :: thesis:
thus ( f . i in dom q1 implies y = f . i ) by A46; :: thesis:
assume not f . i in dom q1 ; :: thesis:
let t be Element of NAT ; :: thesis:
assume t = f . i ; :: thesis:
hence y = t - 1 ; :: thesis:

end;

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

end;

consider gg being FinSequence such that
A54: dom gg = Seg k and
A55: for i being Nat st i in Seg k holds
S₃[i,gg . i] from FINSEQ_1:sch 1(A44);

A56: now

let i, l be Element of NAT ; :: thesis:
assume that
A57: l = f . i and
A58: not f . i in dom q1 and
A59: i in dom gg ; :: thesis:
A60: f . i in rng f by A11, A40, A54, A59, FUNCT_1:def 5;
( l < 1 or m1 < l ) by A42, A57, A58, FINSEQ_1:3;
then A61: m1 + 1 <= l by A11, A57, A60, FINSEQ_1:3, NAT_1:13;

now

assume m1 + 1 = l ; :: thesis:
then k + 1 = i by A9, A11, A14, A40, A54, A57, A59, FUNCT_1:def 8;
then k + 1 <= k + 0 by A54, A59, FINSEQ_1:3;
hence contradiction by XREAL_1:8; :: thesis:

end;

then m1 + 1 < l by A61, XXREAL_0:1;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; :: thesis:

end;

A62: rng gg c= dom p

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng gg ; :: thesis:
then consider x being set such that
A63: x in findom gg and
A64: gg . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A63, SETWISEO:14;

now

per cases ;

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

then A66: f . x = gg . x by A54, A55, A63;
dom q1 c= dom p by A39, A42, A43, FINSEQ_1:7;
hence y in dom p by A64, A65, A66; :: thesis:

end;

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

reconsider j = f . x as Element of NAT by A11, A40, A41, A54, A63;
( j < 1 or m1 < j ) by A42, A67, FINSEQ_1:3;
then A68: ( ( j = 0 or m1 < j ) & f . x in Seg (k + 1) ) by A11, A40, A54, A63, FUNCT_1:def 5, NAT_1:14;
then reconsider l = j - 1 as Element of NAT by FINSEQ_1:3, NAT_1:20;
A69: gg . x = j - 1 by A54, A55, A63, A67;
m1 + 2 <= j by A56, A63, A67;
then (m1 + 2) - 1 <= l by XREAL_1:11;
then ( m1 + 1 <= l & 1 <= m1 + 1 ) by NAT_1:12;
then A70: 1 <= l by XXREAL_0:2;
j <= k + 1 by A68, FINSEQ_1:3;
then l <= (k + 1) - 1 by XREAL_1:11;
hence y in dom p by A43, A64, A69, A70, FINSEQ_1:3; :: thesis:

end;

hence y in dom p ; :: thesis:

end;

( dom p = {} implies dom p = {} ) ;
then reconsider gg = gg as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A43, A54, A62, FUNCT_2:def 1, RELSET_1:11;
A71: rng gg = dom (q1 ^ q2)

proof

thus rng gg c= dom (q1 ^ q2) by A43, A62; :: according to XBOOLE_0:def 10 :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A72: y in dom (q1 ^ q2) ; :: thesis:
then consider x being set such that
A73: x in dom f and
A74: f . x = y by A11, A40, A43, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A11, A73;
reconsider j = y as Element of NAT by A72;

now

per cases ;

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

now

per cases ;

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

then gg . x = f . x by A54, A55, A75;
hence y in rng gg by A74, A75, FUNCT_1:def 5; :: thesis:

end;

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

j <= k by A43, A72, FINSEQ_1:3;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:9;
then j + 1 in rng f by A11, FINSEQ_1:3;
then consider x1 being set such that
A77: x1 in dom f and
A78: f . x1 = j + 1 by FUNCT_1:def 5;

A79: now

assume not x1 in dom gg ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A10, A54, A77, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:16;
then j + 1 = m1 + 1 by A14, A78, TARSKI:def 1;
then ( 1 <= j & j <= m1 ) by A43, A72, FINSEQ_1:3;
hence contradiction by A42, A74, A76, FINSEQ_1:3; :: thesis:

end;

( j < 1 or m1 < j ) by A42, A74, A76, FINSEQ_1:3;
then not j + 1 <= m1 by A43, A72, FINSEQ_1:3, NAT_1:13;
then ( not f . x1 in dom q1 & x1 is Element of NAT ) by A11, A42, A77, A78, FINSEQ_1:3;
then gg . x1 = (j + 1) - 1 by A54, A55, A78, A79
.= y ;
hence y in rng gg by A79, FUNCT_1:def 5; :: thesis:

end;

hence y in rng gg ; :: thesis:

end;

suppose not x in dom gg ; :: thesis:

then x in (Seg (k + 1)) \ (Seg k) by A10, A54, A73, XBOOLE_0:def 5;
then x in {(k + 1)} by FINSEQ_3:16;
then A80: x = k + 1 by TARSKI:def 1;
j <= k by A43, A72, FINSEQ_1:3;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:9;
then j + 1 in rng f by A11, FINSEQ_1:3;
then consider x1 being set such that
A81: x1 in dom f and
A82: f . x1 = j + 1 by FUNCT_1:def 5;

A83: now

assume not x1 in dom gg ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A10, A54, A81, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:16;
then j + 1 = j + 0 by A74, A80, A82, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

m1 <= j by A14, A74, A80, XREAL_1:31;
then not j + 1 <= m1 by NAT_1:13;
then ( not f . x1 in dom q1 & x1 is Element of NAT ) by A11, A42, A81, A82, FINSEQ_1:3;
then gg . x1 = (j + 1) - 1 by A54, A55, A82, A83
.= y ;
hence y in rng gg by A83, FUNCT_1:def 5; :: thesis:

end;

hence y in rng gg ; :: thesis:

end;

gg is one-to-one

proof

let y1 be set ; :: according to FUNCT_1:def 8 :: thesis:
let y2 be set ; :: thesis:
assume that
A84: ( y1 in dom gg & y2 in dom gg ) and
A85: gg . y1 = gg . y2 ; :: thesis:
reconsider j1 = y1, j2 = y2 as Element of NAT by A54, A84;
A86: ( f . y1 in Seg (k + 1) & f . y2 in Seg (k + 1) ) by A11, A40, A54, A84, FUNCT_1:def 5;
then reconsider a = f . y1, b = f . y2 as Element of NAT ;

now

per cases ;

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

then ( gg . j1 = f . y1 & gg . j2 = f . y2 ) by A54, A55, A84;
hence y1 = y2 by A11, A40, A54, A84, A85, FUNCT_1:def 8; :: thesis:

end;

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

then A88: ( gg . j1 = a & gg . j2 = b - 1 ) by A54, A55, A84;
( a <= m1 & 1 <= b ) by A42, A86, A87, FINSEQ_1:3;
then ( (b - 1) + 1 <= m1 + 1 & 1 <= b ) by A85, A88, XREAL_1:8;
then ( b in Seg (m1 + 1) & not b in Seg m1 ) by A6, A26, A87, FINSEQ_1:3, FINSEQ_1:21;
then b in (Seg (m1 + 1)) \ (Seg m1) by XBOOLE_0:def 5;
then b in {(m1 + 1)} by FINSEQ_3:16;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by A9, A11, A14, A40, A54, A84, FUNCT_1:def 8;
hence y1 = y2 by A54, A84, FINSEQ_3:9; :: thesis:

end;

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

then A90: ( gg . j1 = a - 1 & gg . j2 = b ) by A54, A55, A84;
( b <= m1 & 1 <= a ) by A42, A86, A89, FINSEQ_1:3;
then ( (a - 1) + 1 <= m1 + 1 & 1 <= a ) by A85, A90, XREAL_1:8;
then ( a in Seg (m1 + 1) & not a in Seg m1 ) by A6, A26, A89, FINSEQ_1:3, FINSEQ_1:21;
then a in (Seg (m1 + 1)) \ (Seg m1) by XBOOLE_0:def 5;
then a in {(m1 + 1)} by FINSEQ_3:16;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by A9, A11, A14, A40, A54, A84, FUNCT_1:def 8;
hence y1 = y2 by A54, A84, FINSEQ_3:9; :: thesis:

end;

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

then ( gg . j1 = a - 1 & gg . j2 = b - 1 ) by A54, A55, A84;
then ( gg . j1 = a + (- 1) & gg . y2 = b + (- 1) ) ;
then a = b by A85, XCMPLX_1:2;
hence y1 = y2 by A11, A40, A54, A84, FUNCT_1:def 8; :: thesis:

end;

hence y1 = y2 ; :: thesis:

end;

then reconsider gg = gg as Permutation of (dom (q1 ^ q2)) by A71, FUNCT_2:83;

A91: now

let i be Element of NAT ; :: thesis:
assume A92: i in dom p ; :: thesis:
then f . i in rng f by A11, A40, A43, FUNCT_1:def 5;
then reconsider j = f . i as Element of NAT by A11;

now

per cases ;

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

then ( f . i = gg . i & H2 . i = p . i & H1 . j = q1 . j & H2 . i = H1 . (f . i) & q1 . j = (q1 ^ q2) . j ) by A8, A10, A40, A43, A55, A92, FINSEQ_1:def 7, FUNCT_1:70;
hence p . i = (q1 ^ q2) . (gg . i) ; :: thesis:

end;

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

then A94: ( gg . i = j - 1 & H2 . i = p . i & H2 . i = H1 . (f . i) ) by A8, A10, A40, A43, A55, A92, FUNCT_1:70;
then A95: j - 1 in dom (q1 ^ q2) by A43, A54, A71, A92, FUNCT_1:def 5;
m1 + 2 <= j by A43, A54, A56, A92, A93;
then (m1 + 2) - 1 <= j - 1 by XREAL_1:11;
then ( m1 < m1 + 1 & m1 + 1 <= j - 1 ) by XREAL_1:31;
then A96: ( m1 < j - 1 & j - 1 < j ) by XREAL_1:148, XXREAL_0:2;
then m1 < j by XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
not j1 in dom q1 by A42, A96, FINSEQ_1:3;
then consider a being Nat such that
A97: a in dom q2 and
A98: j1 = (len q1) + a by A95, FINSEQ_1:38;
A99: ( H1 = q1 ^ (<*d*> ^ q2) & j in dom H1 ) by A10, A11, A38, A40, A43, A92, FINSEQ_1:45, FUNCT_1:def 5;
then consider b being Nat such that
A100: b in dom (<*d*> ^ q2) and
A101: j = (len q1) + b by A93, FINSEQ_1:38;
A102: ( (q1 ^ q2) . (j - 1) = q2 . a & H1 . j = (<*d*> ^ q2) . b ) by A97, A98, A99, A100, A101, FINSEQ_1:def 7;
A103: b = 1 + a by A98, A101;
len <*d*> = 1 by FINSEQ_1:56;
hence p . i = (q1 ^ q2) . (gg . i) by A94, A97, A102, A103, FINSEQ_1:def 7; :: thesis:

end;

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

end;

now

per cases ;

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

then A105: len p >= 1 by NAT_1:14;
then A106: g "**" p = g "**" (q1 ^ q2) by A5, A14, A16, A25, A28, A91;
H2 = p ^ <*d*> by A6, A7, FINSEQ_3:61;
then A107: g "**" H2 = g . (g "**" (q1 ^ q2)),d by A105, A106, Th5;

now

per cases ;

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

then A108: ( len q1 >= 1 & len q2 >= 1 ) by NAT_1:14;
( len (<*d*> ^ q2) = (len <*d*>) + (len q2) & len <*d*> = 1 ) by FINSEQ_1:35, FINSEQ_1:57;
then A109: len (<*d*> ^ q2) >= 1 by NAT_1:12;
g "**" H2 = g . (g . (g "**" q1),(g "**" q2)),d by A1, A107, A108, Th6
.= 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, A108, Th7
.= g "**" (q1 ^ (<*d*> ^ q2)) by A1, A108, A109, Th6
.= g "**" H1 by A38, FINSEQ_1:45 ;
hence g "**" H1 = g "**" H2 ; :: thesis:

end;

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

then A110: q1 = {} ;
then A111: H1 = <*d*> ^ q2 by A38, FINSEQ_1:47
.= <*d*> ^ (q1 ^ q2) by A110, FINSEQ_1:47 ;
g "**" H2 = g . d,(g "**" (q1 ^ q2)) by A2, A107, BINOP_1:def 2
.= g "**" (<*d*> ^ (q1 ^ q2)) by A1, A14, A16, A25, A28, A105, Th7 ;
hence g "**" H1 = g "**" H2 by A111; :: thesis:

end;

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

then A112: q2 = {} ;
then H1 = q1 ^ <*d*> by A38, FINSEQ_1:47
.= (q1 ^ q2) ^ <*d*> by A112, FINSEQ_1:47 ;
hence g "**" H1 = g "**" H2 by A14, A16, A25, A28, A105, A107, Th5; :: thesis:

end;

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

then len (q1 ^ q2) = 0 + 0 by FINSEQ_1:35;
hence g "**" H1 = g "**" H2 by A6, A7, A14, A16, A28, A104, FINSEQ_1:21; :: thesis:

end;

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

end;

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

then ( dom H1 = {1} & {1} <> {} ) by A6, A25, FINSEQ_1:4, FINSEQ_1:def 3;
then ( dom f = {1} & rng f = {1} & 1 in {1} ) by FUNCT_2:def 1, FUNCT_2:def 3, TARSKI:def 1;
then f . 1 in {1} by FUNCT_1:def 5;
then ( H1 . 1 = H2 . 1 & H2 . 1 = d ) by A13, A25, A113, TARSKI:def 1;
then ( H1 = <*d*> & H2 = <*d*> & g "**" <*d*> = d ) by A6, A7, A25, A113, Lm4, FINSEQ_1:57;
hence g "**" H1 = g "**" H2 ; :: thesis:

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
hence ( len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G ) ; :: thesis: