let m be Nat; :: thesis:
let D be non empty set ; :: thesis:
let A, M be BinOp of D; :: thesis:
let F be finite set ; :: thesis:
assume A1: ( A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A ) ; :: thesis:
set I = the_inverseOp_wrt A;
let E be Enumeration of F; :: thesis:
assume A2: union F c= Seg (1 + m) ; :: thesis:
set EF = Ext (F,(1 + m),(2 + m));
set SF = swap (F,(1 + m),(2 + m));
let Ee be Enumeration of Ext (F,(1 + m),(2 + m)); :: thesis:
let Es be Enumeration of swap (F,(1 + m),(2 + m)); :: thesis:
assume A3: ( Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) ) ; :: thesis:
let Ees be Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))); :: thesis:
assume A4: Ees = Ee ^ Es ; :: thesis:
let s1, s2 be FinSequence; :: thesis:
assume A5: ( s1 in doms ((m + 1),(card F)) & s2 in doms ((m + 1),(card F)) & s1 is with_evenly_repeated_values & s2 is with_evenly_repeated_values & card (s1 " {(1 + m)}) < card (s2 " {(1 + m)}) ) ; :: thesis:
A6: ( card F = len E & len s1 = card F & card F = len s2 ) by A5, CARD_1:def 7;
card (s1 " {(1 + m)}) is even by A5;
then consider n1 being Nat such that
A7: card (s1 " {(1 + m)}) = 2 * n1 by ABIAN:def 2;
card (s2 " {(1 + m)}) is even by A5;
then consider n2 being Nat such that
A8: card (s2 " {(1 + m)}) = 2 * n2 by ABIAN:def 2;
reconsider N = (2 * n2) - (2 * n1) as even Nat by A5, A7, A8, NAT_1:21;
A9: N <> 0 by A5, A7, A8;
set N1 = N |-> (1 + m);
card (dom s2) = card (Seg (len s2)) by FINSEQ_1:def 3
.= len s2 ;
then A10: 2 * n2 <= len s2 by A8, RELAT_1:132, NAT_1:43;
N <= N + (2 * n1) by NAT_1:11;
then reconsider L = (len s2) - N as Nat by A10, XXREAL_0:2, NAT_1:21;
A11: F <> {} by A5;
ex p2 being Permutation of (dom s2) ex s3 being FinSequence st s2 * p2 = s3 ^ (N |-> (1 + m))

not s2 " {(1 + m)} is empty by A5;
then consider x being object such that
A12: x in s2 " {(1 + m)} ;
( x in dom s2 & s2 . x in {(1 + m)} ) by A12, FUNCT_1:def 7;
then ( 1 + m = s2 . x & s2 . x in rng s2 ) by FUNCT_1:def 3, TARSKI:def 1;
then reconsider L = {(1 + m)} as Subset of (rng s2) by ZFMISC_1:31;
(L `) ` = L ;
then consider p being Permutation of (dom s2) such that
A13: (s2 - L) ^ (s2 - (L `)) = s2 * p by FINSEQ_3:115;
L ` = (rng s2) \ L by SUBSET_1:def 4;
then s2 " (L `) = (s2 " (rng s2)) \ (s2 " L) by FUNCT_1:69;
then s2 " (L `) = (dom s2) \ (s2 " L) by RELAT_1:134;
then card (s2 " (L `)) = (card (dom s2)) - (card (s2 " L)) by RELAT_1:132, CARD_2:44;
then card (s2 " (L `)) = (card (Seg (len s2))) - (card (s2 " L)) by FINSEQ_1:def 3;
then A14: len (s2 - (L `)) = (len s2) - ((len s2) - (2 * n2)) by A8, FINSEQ_3:59;
rng (s2 - (L `)) = (rng s2) \ (L `) by FINSEQ_3:65
.= (rng s2) \ ((rng s2) \ L) by SUBSET_1:def 4
.= (rng s2) /\ L by XBOOLE_1:48
.= L by XBOOLE_1:28 ;
then s2 - (L `) = (dom (s2 - (L `))) --> (1 + m) by FUNCOP_1:9;
then s2 - (L `) = (2 * n2) |-> (1 + m) by A14, FINSEQ_1:def 3;
then s2 - (L `) = ((2 * n1) |-> (1 + m)) ^ (N |-> (1 + m)) by FINSEQ_2:123;
then s2 * p = ((s2 - L) ^ ((2 * n1) |-> (1 + m))) ^ (N |-> (1 + m)) by A13, FINSEQ_1:32;
hence ex p2 being Permutation of (dom s2) ex s3 being FinSequence st s2 * p2 = s3 ^ (N |-> (1 + m)) ; :: thesis:

end;

then consider p2 being Permutation of (dom s2), s3 being FinSequence such that
A15: s2 * p2 = s3 ^ (N |-> (1 + m)) ;
A16: dom s2 = dom E by A6, FINSEQ_3:29;
then reconsider Ep = E * p2 as Enumeration of F by Th109;
A17: ( dom p2 = dom s2 & dom s2 = rng p2 ) by FUNCT_2:52, FUNCT_2:def 3;
then A18: dom Ep = dom s2 by RELAT_1:27, A16;
then A19: len Ep = len s2 by FINSEQ_3:29;
set ep1 = Ep | L;
L <= L + N by NAT_1:11;
then A20: len (Ep | L) = L by A19, FINSEQ_1:59;
consider ep2 being FinSequence such that
A21: Ep = (Ep | L) ^ ep2 by FINSEQ_1:80;
set R1 = rng (Ep | L);
set R2 = rng ep2;
A22: len Ep = (len (Ep | L)) + (len ep2) by A21, FINSEQ_1:22;
A23: ( Ep | L is one-to-one & ep2 is one-to-one & rng (Ep | L) misses rng ep2 ) by A21, FINSEQ_3:91;
then reconsider Ep1 = Ep | L as Enumeration of rng (Ep | L) by RLAFFIN3:def 1;
reconsider Ep2 = ep2 as Enumeration of rng ep2 by A23, RLAFFIN3:def 1;
reconsider s2p2 = s2 * p2 as FinSequence ;
s2 * p2 is with_evenly_repeated_values by A5, Th44;
then A24: s3 is with_evenly_repeated_values by A15, Th105;
A25: dom s2p2 = dom s2 by A17, RELAT_1:27;
(N |-> (1 + m)) " {(1 + m)} = Seg N by FUNCOP_1:15;
then A26: card ((N |-> (1 + m)) " {(1 + m)}) = N ;
s2p2,s2 are_fiberwise_equipotent by A25, CLASSES1:80;
then card (s2p2 " {(1 + m)}) = card (s2 " {(1 + m)}) by CLASSES1:78;
then A27: 2 * n2 = (card (s3 " {(1 + m)})) + N by A26, A15, A8, FINSEQ_3:57;
A28: ( (rng (Ep | L)) \/ (rng ep2) = rng Ep & rng Ep = F ) by A21, FINSEQ_1:31, RLAFFIN3:def 1;
( union (rng (Ep | L)) c= union F & union (rng ep2) c= union F ) by A28, XBOOLE_1:7, ZFMISC_1:77;
then A29: ( union (rng (Ep | L)) c= Seg (1 + m) & union (rng ep2) c= Seg (1 + m) ) by A2;
set Rs1 = swap ((rng (Ep | L)),(1 + m),(2 + m));
set Rs2 = swap ((rng ep2),(1 + m),(2 + m));
set Es1 = Swap (Ep1,(1 + m),(2 + m));
set Es2 = Swap (Ep2,(1 + m),(2 + m));
1 + m < (1 + m) + 1 by NAT_1:13;
then A30: ( not 2 + m in union (rng (Ep | L)) & not 2 + m in union (rng ep2) & not 2 + m in union F ) by A2, A29, FINSEQ_1:1;
then reconsider Es1 = Swap (Ep1,(1 + m),(2 + m)) as Enumeration of swap ((rng (Ep | L)),(1 + m),(2 + m)) by Th27;
reconsider Es2 = Swap (Ep2,(1 + m),(2 + m)) as Enumeration of swap ((rng ep2),(1 + m),(2 + m)) by A30, Th27;
A31: 1 + m <> 2 + m ;
then reconsider Ees1 = Ee ^ Es1 as Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m))) by Th79, A30, Th22;
A32: len Ees1 = (len Ee) + (len Es1) by FINSEQ_1:22;
A33: ( len Ee = len E & len E = card F ) by A3, CARD_1:def 7;
set ER1 = Ext ((rng (Ep | L)),(1 + m),(2 + m));
set ER2 = Ext ((rng ep2),(1 + m),(2 + m));
set Ee1 = Ext (Ep1,(1 + m),(2 + m));
set Ee2 = Ext (Ep2,(1 + m),(2 + m));
reconsider Ee1 = Ext (Ep1,(1 + m),(2 + m)) as Enumeration of Ext ((rng (Ep | L)),(1 + m),(2 + m)) by A30, Th28;
reconsider Ee2 = Ext (Ep2,(1 + m),(2 + m)) as Enumeration of Ext ((rng ep2),(1 + m),(2 + m)) by A30, Th28;
reconsider Ees2 = Ee1 ^ Es as Enumeration of (Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) by A31, A30, Th22, Th79;
A34: len (N |-> (1 + m)) = N ;
A35: ( len Ep1 = card (rng (Ep | L)) & len Ep2 = card (rng ep2) ) by CARD_1:def 7;
A36: s3 ^ (N |-> (1 + m)) in doms ((m + 1),((card (rng (Ep | L))) + (card (rng ep2)))) by A35, A22, A19, A6, A15, A5, Th124, A16;
A37: ( s3 in doms ((m + 1),(card (rng (Ep | L)))) & N |-> (1 + m) in doms ((m + 1),(card (rng ep2))) ) by A22, A20, A19, A36, A34, A35, Th120;
A38: card F = (card (rng (Ep | L))) + (card (rng ep2)) by A6, A22, A35, A18, FINSEQ_3:29;
consider S1 being Subset of (doms ((m + 2),((card F) + (card (rng (Ep | L)))))) such that
( card (s1 " {(1 + m)}) = 0 implies s1 ^ s3 in S1 ) and
A40: S1 is with_evenly_repeated_values-member and
A41: for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1 holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap ((rng (Ep | L)),(1 + (len f)),(2 + (len f))))))) * Ees1 holds
for Sd being Element of Fin (dom (App CFes)) st S1 = Sd holds
( M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s3)) = A $$ (Sd,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in Sd & i in dom h holds
( ( (s1 ^ s3) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s3) . i <> 1 + (len f) implies h . i = (s1 ^ s3) . i ) ) ) ) by Th126, A1, A2, A3, A27, A7, A29, A24, A5, Th40, A37;
consider S2 being Subset of (doms ((m + 2),((card (rng (Ep | L))) + (card F)))) such that
( card (s3 " {(1 + m)}) = 0 implies s3 ^ s1 in S2 ) and
A43: S2 is with_evenly_repeated_values-member and
A44: for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1 & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees2 holds
for Sd being Element of Fin (dom (App CFes)) st S2 = Sd holds
( M . (((M "**" (App CE1)) . s3),((M "**" (App CE2)) . s1)) = A $$ (Sd,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in Sd & i in dom h holds
( ( (s3 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s3 ^ s1) . i <> 1 + (len f) implies h . i = (s3 ^ s1) . i ) ) ) ) by Th126, A24, A5, Th40, A1, A2, A3, A27, A7, A29, A37;
consider G, H being Subset of (doms ((m + 2),(card (rng ep2)))) such that
A45: ( G c= (len Ep2) -tuples_on {(1 + m),(2 + m)} & H c= (len Ep2) -tuples_on {(1 + m),(2 + m)} & G is with_evenly_repeated_values-member & H is with_evenly_repeated_values-member ) and
A46: for CFe, CFs being non-empty non empty FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + (len f)),(2 + (len f)))))) * Ee2 & CFs = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + (len f)),(2 + (len f)))))) * Es2 holds
for Se being Element of Fin (dom (App CFe))
for Ss being Element of Fin (dom (App CFs)) st Se = G & Ss = H holds
A . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng ep2))) * Ep2))) . ((len Ep2) |-> (1 + (len f)))),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng ep2))) * Ep2))) . ((len Ep2) |-> (1 + (len f))))) = A . ((A $$ (Se,(M "**" (App CFe)))),(A $$ (Ss,(M "**" (App CFs))))) by A1, Th137, A22, A20, A19, A29;
A47: len Ees2 = (len Ee1) + (len Es) by FINSEQ_1:22;
A48: ( len Es = len E & len E = card F ) by A3, CARD_1:def 7;
(Ext ((rng ep2),(1 + m),(2 + m))) \/ (Ext ((rng (Ep | L)),(1 + m),(2 + m))) = Ext (F,(1 + m),(2 + m)) by A28, Th16;
then A49: (Ext ((rng ep2),(1 + m),(2 + m))) \/ ((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))) = (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) by XBOOLE_1:4;
A50: Ext ((rng ep2),(1 + m),(2 + m)) misses Ext ((rng (Ep | L)),(1 + m),(2 + m)) by A30, A23, Th33;
Ext ((rng ep2),(1 + m),(2 + m)) misses swap (F,(1 + m),(2 + m)) by A31, A30, Th22;
then reconsider Ee2es2 = Ee2 ^ Ees2 as Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) by A49, Th79, A50, XBOOLE_1:70;
A51: len Ee2es2 = (len Ee2) + (len Ees2) by FINSEQ_1:22;
defpred S₁[ object , object ] means ( ( $1 in Seg (L + N) implies for i being Nat st i = (p2 ") . $1 holds
( ( i <= L implies $2 = i + N ) & ( i > L implies $2 = i - L ) ) ) & ( not $1 in Seg (L + N) implies $2 = $1 ) );
A52: ( dom (p2 ") = rng p2 & rng (p2 ") = dom p2 ) by FUNCT_1:33;
A53: len Ees = (len Ee) + (len Es) by FINSEQ_1:22, A4;
A54: ( len Ees = (len s1) + (len s2) & (len s1) + (len s2) = len (s2 ^ s1) ) by A3, CARD_1:def 7, A6, FINSEQ_1:22, A4;
then A55: dom Ees = dom (s2 ^ s1) by FINSEQ_3:29;
A56: len Ee = L + N by A6, A3, CARD_1:def 7;
A57: ( dom s2 = dom Ee & dom Ee = Seg (L + N) ) by A6, A33, FINSEQ_1:def 3, FINSEQ_3:29;
A58: ( dom s2 = dom Ee & dom Ee = Seg (L + N) ) by A6, A33, FINSEQ_1:def 3, FINSEQ_3:29;
A59: dom Ee c= dom Ees by A4, FINSEQ_1:26;
A60: for x being object st x in dom Ees holds
ex y being object st
( y in dom Ees & S₁[x,y] )

proof

let y be object ; :: thesis:
assume A61: y in dom Ees ; :: thesis:
reconsider x = y as Nat by A61;

per cases ;

suppose A62: x in dom Ee ; :: thesis:

then A63: (p2 ") . x in Seg (L + N) by A57, A52, FUNCT_1:def 3, A17;
reconsider j = (p2 ") . x as Nat ;
A64: ( 1 <= j & j <= L + N ) by A63, FINSEQ_1:1;

per cases ;

suppose A65: j <= L ; :: thesis:

then ( 1 + 0 <= j + N & j + N <= L + N ) by XREAL_1:7, A64;
then A66: j + N in dom Ee by A57;
take jN = j + N; :: thesis:
thus ( jN in dom Ees & S₁[y,jN] ) by A62, A56, FINSEQ_1:def 3, A65, A66, A59; :: thesis:

end;

suppose A67: j > L ; :: thesis:

then reconsider jL = j - L as Nat by NAT_1:21;
take jL ; :: thesis:
( 0 <> jL & jL <= j - 0 ) by A67, XREAL_1:6;
then ( 1 <= jL & jL <= L + N ) by A64, XXREAL_0:2, NAT_1:14;
then jL in dom Ee by A57;
hence ( jL in dom Ees & S₁[y,jL] ) by A62, A56, FINSEQ_1:def 3, A67, A59; :: thesis:

end;

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

take x ; :: thesis:
thus ( x in dom Ees & S₁[y,x] ) by A56, FINSEQ_1:def 3, A61, A69; :: thesis:

end;

consider perm1 being Function of (dom Ees),(dom Ees) such that
A70: for x being object st x in dom Ees holds
S₁[x,perm1 . x] from FUNCT_2:sch 1(A60);
A71: dom perm1 = dom Ees by FUNCT_2:52;
A72: dom Ees c= rng perm1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A73: x in dom Ees ; :: thesis:
then reconsider x = x as Nat ;

per cases ;

suppose x in dom Ee ; :: thesis:

then A74: ( 1 <= x & x <= L + N ) by FINSEQ_1:1, A57;

per cases ;

suppose x <= N ; :: thesis:

then ( 1 + 0 <= x + L & x + L <= N + L ) by XREAL_1:7, A74;
then x + L in rng (p2 ") by A57, A17, A52;
then consider y being object such that
A75: ( y in dom (p2 ") & (p2 ") . y = x + L ) by FUNCT_1:def 3;
reconsider y = y as Nat by A75;
A76: y in dom Ees by A59, A75, A57;
A77: S₁[y,perm1 . y] by A70, A59, A75, A57;
( x + L >= 1 + L & 1 + L > L ) by A74, NAT_1:13, XREAL_1:6;
then x + L > L by XXREAL_0:2;
then perm1 . y = (x + L) - L by A75, A57, A77;
hence x in rng perm1 by A71, A76, FUNCT_1:def 3; :: thesis:

end;

suppose A78: x > N ; :: thesis:

then reconsider xN = x - N as Nat by NAT_1:21;
A79: ( 0 <> xN & xN <= (L + N) - N & L <= L + N ) by A74, A78, XREAL_1:9, NAT_1:11;
then ( 1 <= xN & xN <= L & xN <= L + N ) by NAT_1:14, XXREAL_0:2;
then xN in rng (p2 ") by A57, A17, A52;
then consider y being object such that
A80: ( y in dom (p2 ") & (p2 ") . y = xN ) by FUNCT_1:def 3;
A81: y in dom Ees by A59, A80, A57;
perm1 . y = xN + N by A80, A57, A81, A70, A79;
hence x in rng perm1 by A71, A81, FUNCT_1:def 3; :: thesis:

end;

suppose not x in dom Ee ; :: thesis:

then perm1 . x = x by A73, A70, A57;
hence x in rng perm1 by A73, A71, FUNCT_1:def 3; :: thesis:

end;

then dom Ees = rng perm1 ;
then A82: perm1 is onto by FUNCT_2:def 3;
card (dom Ees) = card (dom Ees) ;
then perm1 is one-to-one by A82, FINSEQ_4:63;
then reconsider perm1 = perm1 as Permutation of (dom Ees) by A82;
set p1I = perm1;
A83: ( len Ee1 = len Ep1 & len Ee2 = len Ep2 ) by CARD_1:def 7;
A84: dom Ees = dom Ee2es2 by FINSEQ_3:29, A33, A6, A53, A51, A47, A22, A19, A83;
then A85: dom (Ee2es2 * perm1) = dom perm1 by RELAT_1:27, A72;
then dom (Ee2es2 * perm1) = Seg (len Ees) by A71, FINSEQ_1:def 3;
then reconsider Eperm = Ee2es2 * perm1 as FinSequence by FINSEQ_1:def 2;
for i being Nat st 1 <= i & i <= len Ees holds
Ees . i = Eperm . i

proof

let i be Nat; :: thesis:
assume A86: ( 1 <= i & i <= len Ees ) ; :: thesis:
A87: i in dom Ees by A86, FINSEQ_3:25;
then A88: ( (Ee2es2 * perm1) . i = Ee2es2 . (perm1 . i) & perm1 . i in dom Ee2es2 ) by FUNCT_1:11, FUNCT_1:12, A85, A71;
A89: S₁[i,perm1 . i] by A87, A70;

per cases ;

suppose A90: i in Seg (L + N) ; :: thesis:

reconsider j = (p2 ") . i as Nat ;
A91: Ees . i = Ee . i by A4, A90, A57, FINSEQ_1:def 7;
A92: ( p2 . j = i & j in dom p2 ) by A90, A57, A17, FUNCT_1:32;
A93: ( 1 <= j & j <= L + N ) by A92, FINSEQ_3:25;

per cases ;

suppose A94: j <= L ; :: thesis:

then A95: perm1 . i = j + N by A87, A70, A90;
A96: ( j in dom Ee1 & dom Ee1 c= dom Ees2 ) by A93, A94, A83, A20, FINSEQ_3:25, FINSEQ_1:26;
then A97: (Ee2es2 * perm1) . i = Ees2 . j by A95, A88, A83, A22, A20, A19, FINSEQ_1:def 7
.= Ee1 . j by A96, FINSEQ_1:def 7 ;
Ee1 = (Ext (Ep,(1 + m),(2 + m))) | (Seg L) by Th26;
then Ee1 = (Ee * p2) | (Seg L) by A3, Th25;
then ( j in dom (Ee * p2) & Ee1 . j = (Ee * p2) . j ) by A96, RELAT_1:57, FUNCT_1:47;
hence Ees . i = Eperm . i by A91, A97, A92, FUNCT_1:12; :: thesis:

end;

suppose A98: j > L ; :: thesis:

then reconsider jL = j - L as Nat by NAT_1:21;
A99: perm1 . i = jL by A98, A87, A70, A90;
jL <> 0 by A98;
then ( 1 <= jL & jL <= (L + N) - L ) by A93, XREAL_1:6, NAT_1:14;
then A100: jL in dom Ee2 by A83, A22, A20, A19, FINSEQ_3:25;
dom E = dom (Ext (E,(1 + m),(2 + m))) by Def5;
then A101: j in dom ((Ext (E,(1 + m),(2 + m))) * p2) by A90, A16, A57, A92, FUNCT_1:11;
(Ee2es2 * perm1) . i = Ee2 . jL by A88, A99, A100, FINSEQ_1:def 7
.= (Ee1 ^ Ee2) . (jL + L) by A100, FINSEQ_1:def 7, A83, A20
.= (Ext (Ep,(1 + m),(2 + m))) . j by A21, Th19
.= ((Ext (E,(1 + m),(2 + m))) * p2) . j by Th25
.= (Ext (E,(1 + m),(2 + m))) . (p2 . j) by A101, FUNCT_1:12
.= (Ext (E,(1 + m),(2 + m))) . i by A90, A57, A17, FUNCT_1:32
.= Ee . i by A3 ;
hence Ees . i = Eperm . i by A4, A90, A57, FINSEQ_1:def 7; :: thesis:

end;

suppose A102: not i in Seg (L + N) ; :: thesis:

then A103: ( N <= L + N & L + N < i ) by A86, NAT_1:11;
then N < i by XXREAL_0:2;
then not i in dom Ee2 by A83, A22, A20, A19, FINSEQ_3:25;
then consider n being Nat such that
A104: ( n in dom Ees2 & i = (len Ee2) + n ) by A89, A102, A88, FINSEQ_1:25;
L < n by XREAL_1:6, A104, A103, A83, A22, A20, A19;
then not n in dom Ee1 by FINSEQ_3:25, A83, A20;
then consider m being Nat such that
A105: ( m in dom Es & n = (len Ee1) + m ) by A104, FINSEQ_1:25;
thus Eperm . i = Ee2es2 . i by A88, A87, A70, A102
.= Ees2 . n by A104, FINSEQ_1:def 7
.= Es . m by A105, FINSEQ_1:def 7
.= (Ee ^ Es) . ((len Ee) + m) by A105, FINSEQ_1:def 7
.= (Ee ^ Es) . i by A104, A105, A83, A6, A33, A22, A19
.= Ees . i by A4 ; :: thesis:

end;

then A106: Ees = Eperm by A85, FUNCT_2:52, FINSEQ_3:29;
(swap ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap ((rng ep2),(1 + m),(2 + m))) = swap (F,(1 + m),(2 + m)) by A28, Th13;
then A107: ((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))) \/ (swap ((rng ep2),(1 + m),(2 + m))) = (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) by XBOOLE_1:4;
A108: swap ((rng ep2),(1 + m),(2 + m)) misses swap ((rng (Ep | L)),(1 + m),(2 + m)) by A31, A30, A23, Th34;
swap ((rng ep2),(1 + m),(2 + m)) misses Ext (F,(1 + m),(2 + m)) by A31, A30, Th22;
then swap ((rng ep2),(1 + m),(2 + m)) misses (Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m))) by A108, XBOOLE_1:70;
then reconsider Ees1s2 = Ees1 ^ Es2 as Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) by A107, Th79;
A109: len Ees1s2 = (len Ees1) + (len Es2) by FINSEQ_1:22;
defpred S₂[ object , object ] means ( ( $1 in dom s1 implies $2 = $1 ) & ( not $1 in dom s1 implies for i, j being Nat st j = $1 & i = (p2 ") . (j - (len s1)) holds
$2 = i + (len s1) ) );
A110: len Ees = len (s1 ^ s2) by A48, A33, A6, A53, FINSEQ_1:22;
then A111: dom Ees = dom (s1 ^ s2) by FINSEQ_3:29;
A112: len Es = L + N by A6, A3, CARD_1:def 7;
A113: ( dom s1 = dom Es & dom Es = Seg (L + N) ) by A48, FINSEQ_1:def 3, A6, FINSEQ_3:29;
A114: ( dom s2 = dom Ee & dom Ee = Seg (L + N) ) by A6, A33, FINSEQ_1:def 3, FINSEQ_3:29;
A115: ( len Es1 = len Ep1 & len Es2 = len Ep2 ) by CARD_1:def 7;
A116: dom Ees = dom Ees1s2 by A32, A109, A53, FINSEQ_3:29, A48, A6, A22, A19, A115;
A117: Swap (Ep,(1 + m),(2 + m)) = (Swap (E,(1 + m),(2 + m))) * p2 by Th23;
A118: Ees1s2 = Ee ^ (Es1 ^ Es2) by FINSEQ_1:32;
A119: Es1 ^ Es2 = Swap ((Ep1 ^ Ep2),(1 + m),(2 + m)) by Th18
.= Swap (Ep,(1 + m),(2 + m)) by A21 ;
A120: for x being object st x in dom Ees holds
ex y being object st
( y in dom Ees & S₂[x,y] )

proof

let y be object ; :: thesis:
assume A121: y in dom Ees ; :: thesis:
reconsider x = y as Nat by A121;

per cases ;

suppose x in dom Ee ; :: thesis:

hence ex y being object st
( y in dom Ees & S₂[y,y] ) by A121, A114, A113; :: thesis:

end;

suppose A122: not x in dom Ee ; :: thesis:

then consider n being Nat such that
A123: ( n in dom Es & x = (len Ee) + n ) by A121, FINSEQ_1:25, A4;
reconsider j = (p2 ") . n as Nat ;
take J = j + (len s1); :: thesis:
n in Seg (L + N) by A112, A123, FINSEQ_1:def 3;
then j in Seg (L + N) by A52, FUNCT_1:def 3, A17, A58;
hence ( J in dom Ees & S₂[y,J] ) by A113, A122, A123, A4, A56, A6, FINSEQ_1:28, FINSEQ_1:def 3; :: thesis:

end;

consider perm2 being Function of (dom Ees),(dom Ees) such that
A124: for x being object st x in dom Ees holds
S₂[x,perm2 . x] from FUNCT_2:sch 1(A120);
A125: dom perm2 = dom Ees by FUNCT_2:52;
A126: dom Ees c= rng perm2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A127: y in dom Ees ; :: thesis:
reconsider x = y as Nat by A127;
A128: S₂[x,perm2 . x] by A127, A124;

per cases ;

suppose x in dom Ee ; :: thesis:

hence y in rng perm2 by A128, A3, CARD_1:def 7, A6, FINSEQ_3:29, A127, A125, FUNCT_1:def 3; :: thesis:

end;

suppose not x in dom Ee ; :: thesis:

then consider n being Nat such that
A129: ( n in dom Es & x = (len Ee) + n ) by A127, FINSEQ_1:25, A4;
reconsider j = p2 . n as Nat ;
n in Seg (L + N) by A112, A129, FINSEQ_1:def 3;
then A130: j in Seg (L + N) by FUNCT_1:def 3, A17, A58;
then j in dom Es by FINSEQ_1:def 3, A112;
then A131: (len s1) + j in dom Ees by A4, A56, A6, FINSEQ_1:28;
then A132: S₂[(len s1) + j,perm2 . ((len s1) + j)] by A124;
A133: (p2 ") . (((len s1) + j) - (len s1)) = n by A129, FUNCT_1:32, A17, A58, A113;
j > 0 by A130, FINSEQ_1:1;
then (len s1) + j > (len s1) + 0 by XREAL_1:6;
then perm2 . ((len s1) + j) = x by A129, A56, A6, A133, A132, FINSEQ_3:25;
hence y in rng perm2 by A131, A125, FUNCT_1:def 3; :: thesis:

end;

then dom Ees = rng perm2 ;
then A134: perm2 is onto by FUNCT_2:def 3;
card (dom Ees) = card (dom Ees) ;
then perm2 is one-to-one by A134, FINSEQ_4:63;
then reconsider perm2 = perm2 as Permutation of (dom Ees) by A134;
A135: dom s2 = Seg (N + L) by FINSEQ_1:def 3;
A136: dom (Ees1s2 * perm2) = dom perm2 by RELAT_1:27, A126, A116;
dom (Ees1s2 * perm2) = Seg (len Ees) by A136, A125, FINSEQ_1:def 3;
then reconsider Eperm2 = Ees1s2 * perm2 as FinSequence by FINSEQ_1:def 2;
for i being Nat st 1 <= i & i <= len Ees holds
Ees . i = Eperm2 . i

proof

let i be Nat; :: thesis:
assume A137: ( 1 <= i & i <= len Ees ) ; :: thesis:
i in dom Ees by A137, FINSEQ_3:25;
then A138: ( (Ees1s2 * perm2) . i = Ees1s2 . (perm2 . i) & perm2 . i in dom Ees1s2 ) by FUNCT_1:11, FUNCT_1:12, A136, A125;
A139: i in dom perm2 by A137, FINSEQ_3:25, A125;
A140: ( len s1 = len E & len E = len Ee ) by A6, A3, CARD_1:def 7;
A141: dom s1 = dom Ee by FINSEQ_3:29, A6, A3, CARD_1:def 7;
len (Es1 ^ Es2) = (len Es1) + (len Es2) by FINSEQ_1:22;
then A142: dom (Es1 ^ Es2) = dom s2 by A22, A18, CARD_1:def 7, FINSEQ_3:29;

per cases ;

suppose A143: i in dom s1 ; :: thesis:

( Ees1s2 . i = Ee . i & Ee . i = Ees . i ) by A118, A4, A143, A141, FINSEQ_1:def 7;
hence Ees . i = Eperm2 . i by A143, A139, A124, A138; :: thesis:

end;

suppose A144: not i in dom s1 ; :: thesis:

then consider m being Nat such that
A145: ( m in dom s2 & i = (len s1) + m ) by A137, FINSEQ_3:25, A111, FINSEQ_1:25;
reconsider j = (p2 ") . m as Nat ;
m = i - (len s1) by A145;
then A146: perm2 . i = j + (len s1) by A144, A139, A124;
A147: ( p2 . j = m & j in dom p2 ) by A145, A17, FUNCT_1:32;
A148: j in dom (Es1 ^ Es2) by A142, A145, A17, FUNCT_1:32;
A149: dom Es = dom s2 by A6, A3, CARD_1:def 7, FINSEQ_3:29;
(Ees1s2 * perm2) . i = (Ee ^ (Es1 ^ Es2)) . (j + (len s1)) by FINSEQ_1:32, A146, A138
.= (Es1 ^ Es2) . j by A148, A140, FINSEQ_1:def 7
.= Es . m by A142, A147, A3, A117, A119, FUNCT_1:12
.= (Ee ^ Es) . i by A145, A149, FINSEQ_1:def 7, A6, A33 ;
hence Ees . i = Eperm2 . i by A4; :: thesis:

end;

then A150: Ees = Eperm2 by A136, FUNCT_2:52, FINSEQ_3:29;
(doms ((m + 2),((card F) + (card (rng (Ep | L)))))) ^ (doms ((m + 2),(card (rng ep2)))) = doms ((m + 2),(((card F) + (card (rng (Ep | L)))) + (card (rng ep2)))) by Th123;
then (doms ((m + 2),((card F) + (card (rng (Ep | L)))))) ^ (doms ((m + 2),(card (rng ep2)))) = doms ((m + 2),((card F) + (card F))) by A38;
then reconsider s1h = S1 ^ H as Subset of (doms ((m + 2),((card F) + (card F)))) by POLNOT_1:16;
A151: len Ees = card ((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))) by CARD_1:def 7;
then A152: card ((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))) = (len s1) + (len s2) by A110, FINSEQ_1:22;
then (card F) + (card F) = card ((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))) by A6;
then reconsider Pgs1 = { (s * perm2) where s is FinSequence of NAT : s in s1h } as Subset of (doms ((m + 2),((card F) + (card F)))) by Th119;
(doms ((m + 2),(card (rng ep2)))) ^ (doms ((m + 2),((card F) + (card (rng (Ep | L)))))) = doms ((m + 2),((card (rng ep2)) + ((card F) + (card (rng (Ep | L)))))) by Th123;
then reconsider gs2 = G ^ S2 as Subset of (doms ((m + 2),((card F) + (card F)))) by A38, POLNOT_1:16;
reconsider Pgs2 = { (s * perm1) where s is FinSequence of NAT : s in gs2 } as Subset of (doms ((m + 2),((card F) + (card F)))) by A152, A6, Th119;
take Pgs1 ; :: thesis:
take Pgs2 ; :: thesis:
for x being Element of s1h st x in s1h holds
dom x = dom Ees

proof

let x be Element of s1h; :: thesis:
assume A153: x in s1h ; :: thesis:
reconsider x = x as FinSequence ;
len x = (card F) + (card F) by A153, CARD_1:def 7;
hence dom x = dom Ees by A151, A152, A6, FINSEQ_3:29; :: thesis:

end;

hence Pgs1 is with_evenly_repeated_values-member by A40, A45, Lm1; :: thesis:
for x being Element of gs2 st x in gs2 holds
dom x = dom Ees

proof

let x be Element of gs2; :: thesis:
assume A154: x in gs2 ; :: thesis:
reconsider x = x as FinSequence ;
len x = (card F) + (card F) by A154, CARD_1:def 7;
hence dom x = dom Ees by A151, A152, A6, FINSEQ_3:29; :: thesis:

end;

hence Pgs2 is with_evenly_repeated_values-member by A43, A45, Lm1; :: thesis:
let CE1, CE2 be FinSequence of D * ; :: thesis:
let f be FinSequence of D; :: thesis:
let d1, d2 be Element of D; :: thesis:
assume that
A155: len f = m and
A156: ( CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E ) ; :: thesis:
set fID = f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>;
set fD = f ^ <*(A . (d1,d2))*>;
set fDD = (f ^ <*d1*>) ^ <*d2*>;
let CFes be non-empty non empty FinSequence of D * ; :: thesis:
assume A157: CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees ; :: thesis:
A158: ( len (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) = (len f) + 1 & (len f) + 1 = len (f ^ <*(A . (d1,d2))*>) ) by FINSEQ_2:16;
A159: ( s1 in doms CE1 & s2 in doms CE2 ) by A5, A156, Th106, A158, A155;
A160: ( len s1 = len CE1 & len CE1 = len E & len E = len CE2 & len CE2 = len s2 ) by A6, A156, CARD_1:def 7;
set CEp1 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1;
set CEp2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng ep2))) * Ep2;
( rng ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1) c= D * & rng ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng ep2))) * Ep2) c= D * ) ;
then reconsider CEp1 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1, CEp2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng ep2))) * Ep2 as FinSequence of D * by FINSEQ_1:def 4;
A161: ( len CEp1 = len Ep1 & len CEp2 = len Ep2 & len (N |-> (1 + m)) = N ) by CARD_1:def 7;
A162: s3 ^ (N |-> (1 + m)) in doms ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep) by A159, A15, A156, Th110, A16;
A163: (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep = CEp1 ^ CEp2 by A21, Th81, A28;
then A164: ( s3 in doms CEp1 & N |-> (1 + m) in doms CEp2 ) by A22, A20, A19, A161, A162, Th50;
A165: s2p2 in dom (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep)) by A15, A162, Def9;
A166: (M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s2 = (M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep))) . s2p2 by A159, A1, A156, Th112, A16
.= M "**" ((App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep)) . s2p2) by A165, Def10
.= M "**" (((App CEp1) . s3) ^ ((App CEp2) . (N |-> (1 + m)))) by A15, A164, A163, Th61
.= M . ((M "**" ((App CEp1) . s3)),(M "**" ((App CEp2) . (N |-> (1 + m))))) by A1, FINSOP_1:5 ;
set CFes1 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1;
set DFs2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2;
A167: len ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) = len Ees1 by CARD_1:def 7;
A168: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ees1 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1) c= D * ;
then reconsider CFes1 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap ((rng (Ep | L)),(1 + m),(2 + m)))))) * Ees1 as non-empty non empty FinSequence of D * by A11, A168, FINSEQ_1:def 4, FUNCT_1:def 9;
A169: len ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) = len Es2 by CARD_1:def 7;
A170: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Es2 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2) c= D * ;
then reconsider DFs2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap ((rng ep2),(1 + m),(2 + m))))) * Es2 as non-empty non empty FinSequence of D * by A9, A22, A20, A19, A170, FINSEQ_1:def 4, FUNCT_1:def 9;
set CFes2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2;
set GFe2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2;
A171: len ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) = len Ees2 by CARD_1:def 7;
A172: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ees2 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2) c= D * ;
then reconsider CFes2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext ((rng (Ep | L)),(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees2 as non-empty non empty FinSequence of D * by A11, A172, FINSEQ_1:def 4, FUNCT_1:def 9;
A173: len ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) = len Ee2 by CARD_1:def 7;
A174: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee2 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2) c= D * ;
then reconsider GFe2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext ((rng ep2),(1 + m),(2 + m))))) * Ee2 as non-empty non empty FinSequence of D * by A9, A22, A20, A19, A174, FINSEQ_1:def 4, FUNCT_1:def 9;
set CGS1 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2;
set DEp1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1;
set DEp2 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng ep2))) * Ep2;
( rng ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1) c= D * & rng ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng ep2))) * Ep2) c= D * ) ;
then reconsider DEp1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1, DEp2 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng ep2))) * Ep2 as FinSequence of D * by FINSEQ_1:def 4;
A175: doms ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E) = doms ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E) by A158, Th107;
then s1 in dom (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E)) by A159, A156, Def9;
then (M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s1 = M "**" ((App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E)) . s1) by Def10;
then reconsider m1 = (M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s1 as Element of D ;
doms ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1) = doms ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1) by A158, Th107;
then A176: s3 in dom (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1)) by A164, Def9;
then (M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3 = M "**" ((App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1)) . s3) by Def10;
then reconsider md3 = (M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3 as Element of D ;
A177: ( len DEp1 = len Ep1 & len DEp2 = len Ep2 & len (N |-> (1 + m)) = N ) by CARD_1:def 7;
doms ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * Ep) = doms ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep) by A158, Th107;
then A178: s3 ^ (N |-> (1 + m)) in doms ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep) by A159, A15, A156, Th110, A16;
A179: (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep = DEp1 ^ DEp2 by A21, A28, Th81;
then A180: ( s3 in doms DEp1 & N |-> (1 + m) in doms DEp2 ) by A178, A177, Th50, A22, A20, A19;
A181: s2p2 in dom (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep)) by A178, A15, Def9;
A182: (M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s2 = (M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep))) . s2p2 by A159, A1, Th112, A16, A175, A156
.= M "**" ((App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * Ep)) . s2p2) by A181, Def10
.= M "**" (((App DEp1) . s3) ^ ((App DEp2) . (N |-> (1 + m)))) by A15, A179, A180, Th61
.= M . ((M "**" ((App DEp1) . s3)),(M "**" ((App DEp2) . (N |-> (1 + m))))) by A1, FINSOP_1:5 ;
s1 in dom (App CE2) by A175, A156, A159, Def9;
then M "**" ((App CE2) . s1) = (M "**" (App CE2)) . s1 by Def10;
then reconsider CE2s1 = (M "**" (App CE2)) . s1 as Element of D ;
s1 in dom (App CE1) by A159, Def9;
then M "**" ((App CE1) . s1) = (M "**" (App CE1)) . s1 by Def10;
then reconsider CE1s1 = (M "**" (App CE1)) . s1 as Element of D ;
A183: s3 in dom (App CEp1) by A164, Def9;
then (M "**" (App CEp1)) . s3 = M "**" ((App CEp1) . s3) by Def10;
then reconsider mc3 = (M "**" (App CEp1)) . s3 as Element of D ;
A184: ( len ((f ^ <*d1*>) ^ <*d2*>) = (len (f ^ <*d1*>)) + 1 & len (f ^ <*d1*>) = m + 1 ) by A155, FINSEQ_2:16;
then dom (App CFes1) = doms ((m + 2),((card F) + (card (rng (Ep | L))))) by Lm3, A32, A33, A115, A35;
then reconsider dS1 = S1 as Element of Fin (dom (App CFes1)) by FINSUB_1:def 5;
dom (App CFes2) = doms ((m + 2),((card (rng (Ep | L))) + (card F))) by Lm3, A184, A35, A47, A48, A83;
then reconsider dS2 = S2 as Element of Fin (dom (App CFes2)) by FINSUB_1:def 5;
A185: DEp1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1 ;
A186: ( M . (((M "**" (App DEp1)) . s3),((M "**" (App CE2)) . s1)) = A $$ (dS2,(M "**" (App CFes2))) & ( for h being FinSequence
for i being Nat st h in dS2 & i in dom h holds
( ( (s3 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s3 ^ s1) . i <> 1 + (len f) implies h . i = (s3 ^ s1) . i ) ) ) ) by A156, A155, A44, A185;
CEp1 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1 ;
then A187: ( M . (((M "**" (App CE1)) . s1),((M "**" (App CEp1)) . s3)) = A $$ (dS1,(M "**" (App CFes1))) & ( for h being FinSequence
for i being Nat st h in dS1 & i in dom h holds
( ( (s1 ^ s3) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s3) . i <> 1 + (len f) implies h . i = (s1 ^ s3) . i ) ) ) ) by A155, A41, A156;
A188: A $$ (dS1,(M "**" (App CFes1))) = M . (((M "**" (App CE1)) . s1),((M "**" (App CEp1)) . s3)) by A155, A41, A156
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s1),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3)) by A156
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s1),((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3)) by A155, A159, A156, A7, A27, A164, A1, Th136
.= M . (md3,m1) by A1, BINOP_1:def 2
.= M . (((M "**" (App DEp1)) . s3),((M "**" (App CE2)) . s1)) by A156
.= A $$ (dS2,(M "**" (App CFes2))) by A156, A155, A44 ;
A189: A $$ (dS1,(M "**" (App CFes1))) = M . (((M "**" (App CE1)) . s1),((M "**" (App CEp1)) . s3)) by A187
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s1),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3)) by A156
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s1),((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(rng (Ep | L)))) * Ep1))) . s3)) by A155, A156, A159, A7, A27, A164, A1, Th136
.= M . (md3,m1) by A1, BINOP_1:def 2
.= M . (((M "**" (App DEp1)) . s3),((M "**" (App CE2)) . s1)) by A156
.= A $$ (dS2,(M "**" (App CFes2))) by A156, A155, A44 ;
A190: M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)) = M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s2),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s1)) by A156
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s2),CE2s1) by A156
.= M . ((M . ((M "**" ((App DEp1) . s3)),(M "**" ((App DEp2) . (N |-> (1 + m)))))),CE2s1) by A182
.= M . ((M . ((M "**" ((App DEp2) . (N |-> (1 + m)))),(M "**" ((App DEp1) . s3)))),CE2s1) by A1, BINOP_1:def 2
.= M . ((M "**" ((App DEp2) . (N |-> (1 + m)))),(M . ((M "**" ((App DEp1) . s3)),CE2s1))) by A1, BINOP_1:def 3
.= M . ((M "**" ((App DEp2) . (N |-> (1 + m)))),(A $$ (dS2,(M "**" (App CFes2))))) by Def10, A176, A186 ;
A191: M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E))) . s1),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s2)) by A156
.= M . (CE1s1,((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s2)) by A156
.= M . (((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E))) . s2),CE1s1) by A1, BINOP_1:def 2, A166
.= M . ((M . ((M "**" ((App CEp1) . s3)),(M "**" ((App CEp2) . (N |-> (1 + m)))))),CE1s1) by A166
.= M . ((M . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(M "**" ((App CEp1) . s3)))),CE1s1) by A1, BINOP_1:def 2
.= M . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(M . ((M "**" ((App CEp1) . s3)),CE1s1))) by A1, BINOP_1:def 3
.= M . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(M . (CE1s1,(M "**" ((App CEp1) . s3))))) by A1, BINOP_1:def 2
.= M . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(A $$ (dS1,(M "**" (App CFes1))))) by A187, A183, Def10 ;
( N |-> (1 + m) in dom (App CEp2) & N |-> (1 + m) in dom (App DEp2) ) by A164, A180, Def9;
then A192: ( M "**" ((App CEp2) . (N |-> (1 + m))) = (M "**" (App CEp2)) . (N |-> (1 + m)) & M "**" ((App DEp2) . (N |-> (1 + m))) = (M "**" (App DEp2)) . (N |-> (1 + m)) ) by Def10;
dom (App GFe2) = doms ((m + 2),(card (rng ep2))) by A83, A35, A184, Lm3;
then reconsider dG = G as Element of Fin (dom (App GFe2)) by FINSUB_1:def 5;
dom (App DFs2) = doms ((m + 2),(card (rng ep2))) by A115, A35, A184, Lm3;
then reconsider dH = H as Element of Fin (dom (App DFs2)) by FINSUB_1:def 5;
A193: CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees by A157, A155;
then A194: len CFes = len Ees by CARD_1:def 7;
doms ((m + 2),((card F) + (card F))) = dom (App CFes) by A193, A184, Lm3, A33, A48, A53;
then reconsider dPgs1 = Pgs1, dPgs2 = Pgs2 as Element of Fin (dom (App CFes)) by FINSUB_1:def 5;
A195: A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A . ((M . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(A $$ (dS2,(M "**" (App CFes2)))))),(M . ((M "**" ((App DEp2) . (N |-> (1 + m)))),(A $$ (dS2,(M "**" (App CFes2))))))) by A189, A190, A191
.= M . ((A . ((M "**" ((App CEp2) . (N |-> (1 + m)))),(M "**" ((App DEp2) . (N |-> (1 + m)))))),(A $$ (dS2,(M "**" (App CFes2))))) by A1, BINOP_1:13
.= M . ((A . ((M "**" ((App DEp2) . (N |-> (1 + m)))),(M "**" ((App CEp2) . (N |-> (1 + m)))))),(A $$ (dS2,(M "**" (App CFes2))))) by A1, BINOP_1:def 2
.= M . ((A . ((A $$ (dG,(M "**" (App GFe2)))),(A $$ (dH,(M "**" (App DFs2)))))),(A $$ (dS2,(M "**" (App CFes2))))) by A192, A155, A46, A22, A20, A19
.= A . ((M . ((A $$ (dG,(M "**" (App GFe2)))),(A $$ (dS2,(M "**" (App CFes2)))))),(M . ((A $$ (dH,(M "**" (App DFs2)))),(A $$ (dS2,(M "**" (App CFes2))))))) by A1, BINOP_1:13 ;
set CGS2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2;
A196: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee2es2 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2) c= D * ;
then reconsider CGS2 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ee2es2 as non-empty non empty FinSequence of D * by A11, A196, FINSEQ_1:def 4, FUNCT_1:def 9;
doms ((m + 2),((card F) + (card F))) = dom (App CGS2) by A184, Lm3, A38, A35, A48, A51, A47, A83;
then reconsider dgs2 = gs2 as Element of Fin (dom (App CGS2)) by FINSUB_1:def 5;
A197: GFe2 ^ CFes2 = CGS2 by A49, Th81;
( dG c= dom (App GFe2) & dS2 c= dom (App CFes2) ) by FINSUB_1:def 5;
then A198: ( dG c= doms GFe2 & dS2 c= doms CFes2 ) by Def9;
A199: ( dPgs2 c= dom (App CFes) & dom (App CFes) = doms CFes ) by Def9, FINSUB_1:def 5;
A200: len s3 = L by A20, A177, A180, Th47;
A201: for h being FinSequence
for i being Nat st h in Pgs2 & i in dom (s2 ^ s1) holds
( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) )

proof

let h be FinSequence; :: thesis:
let i be Nat; :: thesis:
assume A202: ( h in Pgs2 & i in dom (s2 ^ s1) ) ; :: thesis:
consider s being FinSequence of NAT such that
A203: ( h = s * perm1 & s in gs2 ) by A202;
len h = len (s2 ^ s1) by Th47, A194, A54, A199, A202;
then dom h = dom (s2 ^ s1) by FINSEQ_3:29;
then A204: ( h . i = s . (perm1 . i) & i in dom perm1 ) by A203, A202, FUNCT_1:11, FUNCT_1:12;
consider g1, g2 being FinSequence such that
A205: ( s = g1 ^ g2 & g1 in G & g2 in S2 ) by A203, POLNOT_1:def 2;
A206: ( len g1 = len Ee2 & len Ee2 = N & len g2 = (len Ee1) + (len E) ) by Th47, A198, A205, CARD_1:def 7, A48, A47, A171, A173, A22, A20, A19;
then ( len s = (len g1) + (len g2) & (len g1) + (len g2) = (len E) + (len E) ) by FINSEQ_1:22, A205, A6, A83, A20;
then A207: dom s = dom Ees by A3, CARD_1:def 7, A4, FINSEQ_3:29;
A208: S₁[i,perm1 . i] by A55, A202, A70;

per cases ;

suppose A209: i in dom s2 ; :: thesis:

then A210: (s2 ^ s1) . i = s2 . i by FINSEQ_1:def 7;
consider j being object such that
A211: ( j in dom p2 & i = p2 . j ) by A209, A17, FUNCT_1:def 3;
reconsider j = j as Nat by A211;
A212: j in dom (s2 * p2) by A211, A17, RELAT_1:27;
A213: (s3 ^ (N |-> (1 + m))) . j = s2 . i by A25, A15, A211, FUNCT_1:12;
A214: (p2 ") . i = j by A211, FUNCT_1:32;

per cases ;

suppose A215: j in dom s3 ; :: thesis:

then A216: ( 1 <= j & j <= L ) by A200, FINSEQ_3:25;
s2 . i = s3 . j by A213, A215, FINSEQ_1:def 7;
then A217: (s2 ^ s1) . i = (s3 ^ s1) . j by A210, A215, FINSEQ_1:def 7;
A218: dom s3 c= dom g2 by A83, A20, A200, FINSEQ_3:30, A206, NAT_1:11;
A219: s . (j + N) = g2 . j by A218, A215, A206, A205, FINSEQ_1:def 7;
h . i = s . (j + N) by A204, A214, A208, A216, A209, FINSEQ_1:def 3;
hence ( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) ) by A219, A217, A218, A215, A186, A205; :: thesis:

end;

suppose A221: not j in dom s3 ; :: thesis:

then consider n being Nat such that
A222: ( n in dom (N |-> (1 + m)) & j = (len s3) + n ) by A212, A15, FINSEQ_1:25;
j >= 1 by A211, FINSEQ_3:25;
then A223: j > L by A200, A221, FINSEQ_3:25;
A224: perm1 . i = j - L by A223, A214, A208, A209, FINSEQ_1:def 3;
A225: s2 . i = (N |-> (1 + m)) . n by A213, A222, FINSEQ_1:def 7;
thus ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) :: thesis:

proof

assume (s2 ^ s1) . i = 1 + (len f) ; :: thesis:
len g1 = len (N |-> (1 + m)) by A206;
then A226: dom g1 = dom (N |-> (1 + m)) by FINSEQ_3:29;
then A227: h . i = g1 . n by A224, A200, A204, A205, FINSEQ_1:def 7, A222;
g1 is Element of (len Ep2) -tuples_on {(1 + (len f)),(2 + (len f))} by A155, A205, A45;
then A228: rng g1 c= {(1 + (len f)),(2 + (len f))} by FINSEQ_1:def 4;
g1 . n in rng g1 by A226, A222, FUNCT_1:def 3;
hence h . i in {(1 + (len f)),(2 + (len f))} by A227, A228; :: thesis:

end;

thus ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) by A155, A225, A210, A222, FUNCOP_1:7; :: thesis:

end;

suppose A229: not i in dom s2 ; :: thesis:

then consider n being Nat such that
A230: ( n in dom s1 & i = (len s2) + n ) by A202, FINSEQ_1:25;
(s2 ^ s1) . i = s1 . n by A230, FINSEQ_1:def 7;
then A231: (s2 ^ s1) . i = (s3 ^ s1) . (L + n) by A200, A230, FINSEQ_1:def 7;
A232: dom s2 = Seg (L + N) by FINSEQ_1:def 3;
1 <= i by A202, FINSEQ_3:25;
then ( N <= L + N & L + N < i ) by A232, A229, NAT_1:11;
then N < i by XXREAL_0:2;
then A233: not i in dom g1 by FINSEQ_3:25, A206;
consider m being Nat such that
A234: ( m in dom g2 & i = (len g1) + m ) by A207, A55, A202, A205, A233, FINSEQ_1:25;
h . i = g2 . m by FINSEQ_1:def 3, A204, A229, A208, A205, FINSEQ_1:def 7, A234;
hence ( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) ) by A231, A234, A206, A230, A205, A186; :: thesis:

end;

A235: for x being object st x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) holds
not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) ; :: thesis:
then ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) . x = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ees1s2 . x)) by Th80;
hence not ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) . x is empty ; :: thesis:

end;

rng ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2) c= D * ;
then reconsider CGS1 = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees1s2 as non-empty non empty FinSequence of D * by A11, A235, FINSEQ_1:def 4, FUNCT_1:def 9;
doms ((m + 2),((card F) + (card F))) = dom (App CGS1) by A38, A184, Lm3, A115, A35, A32, A33, A109;
then reconsider ds1h = s1h as Element of Fin (dom (App CGS1)) by FINSUB_1:def 5;
A236: CFes1 ^ DFs2 = CGS1 by A107, Th81;
( dH c= dom (App DFs2) & dS1 c= dom (App CFes1) ) by FINSUB_1:def 5;
then A237: ( dH c= doms DFs2 & dS1 c= doms CFes1 ) by Def9;
A238: dPgs1 c= dom (App CFes) by FINSUB_1:def 5;
A239: for h being FinSequence
for i being Nat st h in Pgs1 & i in dom (s1 ^ s2) holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) )

proof

let h be FinSequence; :: thesis:
let i be Nat; :: thesis:
assume A240: ( h in Pgs1 & i in dom (s1 ^ s2) ) ; :: thesis:
consider s being FinSequence of NAT such that
A241: ( h = s * perm2 & s in s1h ) by A240;
len h = len (s1 ^ s2) by Th47, A194, A110, A238, A199, A240;
then A242: dom h = dom (s1 ^ s2) by FINSEQ_3:29;
then A243: ( h . i = s . (perm2 . i) & i in dom perm2 ) by A241, A240, FUNCT_1:11, FUNCT_1:12;
consider g1, g2 being FinSequence such that
A244: ( s = g1 ^ g2 & g1 in S1 & g2 in H ) by A241, POLNOT_1:def 2;
A245: ( len g2 = len DFs2 & len g1 = len CFes1 ) by Th47, A237, A244;
A246: ( len g2 = len Es2 & len g1 = (len Es1) + (len E) ) by A169, A33, A32, A167, Th47, A237, A244;
A247: dom g1 = dom Ees1 by A245, CARD_1:def 7, FINSEQ_3:29;
A248: ( dom s1 = dom Ee & dom Ee c= dom Ees1 ) by A3, CARD_1:def 7, A6, FINSEQ_3:29, FINSEQ_1:26;

per cases ;

suppose A249: i in dom s1 ; :: thesis:

then A250: perm2 . i = i by A124, A111, A240;
A251: s . i = g1 . i by A247, A248, A249, A244, FINSEQ_1:def 7;
( (s1 ^ s3) . i = s1 . i & s1 . i = (s1 ^ s2) . i ) by A249, FINSEQ_1:def 7;
hence ( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) by A243, A250, A251, A187, A247, A248, A249, A244; :: thesis:

end;

suppose A252: not i in dom s1 ; :: thesis:

then consider n being Nat such that
A253: ( n in dom s2 & i = (len s1) + n ) by A240, FINSEQ_1:25;
reconsider j = (p2 ") . n as Nat ;
n = i - (len s1) by A253;
then A254: perm2 . i = j + (len s1) by A124, A111, A240, A252;
A255: ( p2 . j = n & j in dom p2 ) by A253, A17, FUNCT_1:32;
then A256: s2 . n = (s3 ^ (N |-> (1 + m))) . j by A15, A253, FUNCT_1:11, FUNCT_1:12;
A257: ( 1 <= j & j <= L + N ) by A135, A255, FINSEQ_1:1;
A258: (s1 ^ s2) . i = s2 . n by A253, FINSEQ_1:def 7;

per cases ;

suppose A259: j <= L ; :: thesis:

then ( 1 + 0 <= j + (len E) & j + (len E) <= len g1 ) by A257, A245, A33, A32, A167, A115, A20, XREAL_1:7;
then A260: j + (len E) in dom g1 by FINSEQ_3:25;
then A261: h . i = g1 . (j + (len E)) by A254, A243, A244, FINSEQ_1:def 7, A6;
A262: j in dom s3 by A200, A257, A259, FINSEQ_3:25;
then A263: (s1 ^ s3) . (j + (len E)) = s3 . j by FINSEQ_1:def 7, A6;
thus ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) :: thesis:

proof

assume (s1 ^ s2) . i = 1 + (len f) ; :: thesis:
then (s1 ^ s3) . (j + (len E)) = 1 + (len f) by A256, A258, A263, A262, FINSEQ_1:def 7;
hence h . i in {(1 + (len f)),(2 + (len f))} by A261, A244, A260, A187; :: thesis:

end;

assume (s1 ^ s2) . i <> 1 + (len f) ; :: thesis:
then (s1 ^ s3) . (j + (len E)) <> 1 + (len f) by A256, A258, A263, A262, FINSEQ_1:def 7;
then g1 . (j + (len E)) = (s1 ^ s3) . (j + (len E)) by A244, A260, A187;
hence h . i = (s1 ^ s2) . i by A261, A258, A262, A263, A256, FINSEQ_1:def 7; :: thesis:

end;

suppose A264: j > L ; :: thesis:

then reconsider jL = j - L as Nat by NAT_1:21;
jL <> 0 by A264;
then A265: ( 1 <= jL & jL <= (L + N) - L ) by A257, XREAL_1:6, NAT_1:14;
then A266: jL in dom (N |-> (1 + m)) ;
then A267: (s3 ^ (N |-> (1 + m))) . (L + jL) = (N |-> (1 + m)) . jL by A200, FINSEQ_1:def 7;
A268: jL in dom g2 by A115, A22, A20, A19, A246, A265, FINSEQ_3:25;
L + (len s1) = len g1 by A20, A245, A6, A3, CARD_1:def 7, A167;
then A269: ( h . i = s . (jL + (L + (len s1))) & s . (jL + (L + (len s1))) = g2 . jL ) by A244, A254, A242, A241, A240, FUNCT_1:12, A268, FINSEQ_1:def 7;
g2 is Element of (len Ep2) -tuples_on {(1 + (len f)),(2 + (len f))} by A155, A45, A244;
then A270: rng g2 c= {(1 + (len f)),(2 + (len f))} by FINSEQ_1:def 4;
g2 . jL in rng g2 by A268, FUNCT_1:def 3;
hence ( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) by A155, A269, A270, A267, A258, A256, FUNCOP_1:7, A266; :: thesis:

end;

A271: Pgs2 misses Pgs1

proof

assume Pgs2 meets Pgs1 ; :: thesis:
then consider x being object such that
A272: ( x in Pgs2 & x in Pgs1 ) by XBOOLE_0:3;
reconsider x = x as FinSequence by A272;
A273: dom s1 = dom s2 by A6, FINSEQ_3:29;
s1 <> s2 by A5;
then consider i being object such that
A274: ( i in dom s1 & s1 . i <> s2 . i ) by A6, FINSEQ_3:29;
reconsider i = i as Nat by A274;
A275: ( (s1 ^ s2) . i = s1 . i & (s2 ^ s1) . i = s2 . i ) by A274, A273, FINSEQ_1:def 7;
A276: ( dom s1 c= dom (s1 ^ s2) & dom s2 c= dom (s2 ^ s1) ) by FINSEQ_1:26;
( dom s1 = dom CE1 & dom s2 = dom CE2 ) by A160, FINSEQ_3:29;
then A277: ( CE1 . i = SignGen ((f ^ <*(A . (d1,d2))*>),A,(E . i)) & CE2 . i = SignGen ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(E . i)) ) by A156, Th80, A274, A273;

per cases ;

suppose A278: s1 . i = 1 + (len f) ; :: thesis:

then x . i in {(1 + (len f)),(2 + (len f))} by A275, A276, A239, A272, A274;
then A279: ( x . i = 1 + (len f) or x . i = 2 + (len f) ) by TARSKI:def 2;
s2 . i in dom (CE2 . i) by A159, Th47, A274, A273;
then A280: s2 . i in dom (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) by A277, Def11;
x . i = s2 . i by A278, A201, A275, A276, A274, A273, A272;
then (1 + (len f)) + 1 <= len (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) by FINSEQ_3:25, A280, A279, A278, A274;
hence contradiction by A158, NAT_1:13; :: thesis:

end;

suppose A281: s2 . i = 1 + (len f) ; :: thesis:

then x . i in {(1 + (len f)),(2 + (len f))} by A275, A276, A274, A273, A272, A201;
then A282: ( x . i = 1 + (len f) or x . i = 2 + (len f) ) by TARSKI:def 2;
s1 . i in dom (CE1 . i) by A159, Th47, A274;
then A283: s1 . i in dom (f ^ <*(A . (d1,d2))*>) by A277, Def11;
x . i = s1 . i by A239, A276, A272, A281, A275, A274;
then (1 + (len f)) + 1 <= len (f ^ <*(A . (d1,d2))*>) by FINSEQ_3:25, A283, A282, A281, A274;
hence contradiction by A158, NAT_1:13; :: thesis:

end;

suppose ( s1 . i <> 1 + (len f) & s2 . i <> 1 + (len f) ) ; :: thesis:

then ( x . i = s1 . i & x . i = s2 . i ) by A201, A239, A275, A276, A274, A273, A272;
hence contradiction by A274; :: thesis:

end;

let D1, D2 be Element of Fin (dom (App CFes)); :: thesis:
assume A284: ( D1 = Pgs1 & D2 = Pgs2 ) ; :: thesis:
thus D1 misses D2 by A271, A284; :: thesis:
thus A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A . ((M . ((A $$ (dG,(M "**" (App GFe2)))),(A $$ (dS2,(M "**" (App CFes2)))))),(M . ((A $$ (dH,(M "**" (App DFs2)))),(A $$ (dS2,(M "**" (App CFes2))))))) by A195
.= A . ((A $$ (dgs2,(M "**" (App CGS2)))),(M . ((A $$ (dH,(M "**" (App DFs2)))),(A $$ (dS2,(M "**" (App CFes2))))))) by A197, A1, Th93
.= A . ((A $$ (dPgs2,(M "**" (App CFes)))),(M . ((A $$ (dH,(M "**" (App DFs2)))),(A $$ (dS2,(M "**" (App CFes2))))))) by A193, A1, A84, A106, Th115
.= A . ((A $$ (dPgs2,(M "**" (App CFes)))),(M . ((A $$ (dH,(M "**" (App DFs2)))),(A $$ (dS1,(M "**" (App CFes1))))))) by A188
.= A . ((A $$ (dPgs2,(M "**" (App CFes)))),(M . ((A $$ (dS1,(M "**" (App CFes1)))),(A $$ (dH,(M "**" (App DFs2))))))) by A1, BINOP_1:def 2
.= A . ((A $$ (dPgs2,(M "**" (App CFes)))),(A $$ (ds1h,(M "**" (App CGS1))))) by A1, Th93, A236
.= A . ((A $$ (dPgs2,(M "**" (App CFes)))),(A $$ (dPgs1,(M "**" (App CFes))))) by A1, A116, A150, Th115, A193
.= A $$ ((D1 \/ D2),(M "**" (App CFes))) by A284, A271, A1, SETWOP_2:4 ; :: thesis:
thus for h being FinSequence
for i being Nat st h in D1 & i in dom (s1 ^ s2) holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) by A239, A284; :: thesis:
thus for h being FinSequence
for i being Nat st h in D2 & i in dom (s2 ^ s1) holds
( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) ) by A201, A284; :: thesis: