let m be Nat; :: thesis: for D being non empty set
for A, M being BinOp of D
for F being finite set st 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 holds
for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let D be non empty set ; :: thesis: for A, M being BinOp of D
for F being finite set st 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 holds
for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let A, M be BinOp of D; :: thesis: for F being finite set st 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 holds
for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let F be finite set ; :: thesis: ( 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 implies for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) ) )
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: for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let E be Enumeration of F; :: thesis: ( union F c= Seg (1 + m) implies for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) ) )
assume A2: union F c= Seg (1 + m) ; :: thesis: for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let Ee be Enumeration of Ext (F,(1 + m),(2 + m)); :: thesis: for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let Es be Enumeration of swap (F,(1 + m),(2 + m)); :: thesis: ( Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) implies for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) ) )
assume A3: ( Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) ) ; :: thesis: for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let Ees be Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))); :: thesis: ( Ees = Ee ^ Es implies for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) ) )
assume A4: Ees = Ee ^ Es ; :: thesis: for s1, s2 being FinSequence st 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 & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
let s1, s2 be FinSequence; :: thesis: ( 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 & s1 <> s2 implies ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) ) )
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 & s1 <> s2 ) ; :: thesis: ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
set I = the_inverseOp_wrt A;

per cases ( card (s1 " {(1 + m)}) = card (s2 " {(1 + m)}) or card (s1 " {(1 + m)}) < card (s2 " {(1 + m)}) or card (s1 " {(1 + m)}) > card (s2 " {(1 + m)}) ) by XXREAL_0:1;

suppose A6: card (s1 " {(1 + m)}) = card (s2 " {(1 + m)}) ; :: thesis: ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )

then consider D1 being Subset of (doms ((m + 2),((card F) + (card F)))) such that
( card (s1 " {(1 + m)}) = 0 implies s1 ^ s2 in D1 ) and
A7: ( D1 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for Sd being Element of Fin (dom (App CFes)) st Sd = D1 holds
( M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)) = A $$ (Sd,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in Sd & i in dom h 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 A1, A2, A3, A4, A5, Th126, Th40;
consider D2 being Subset of (doms ((m + 2),((card F) + (card F)))) such that
( card (s2 " {(1 + m)}) = 0 implies s2 ^ s1 in D2 ) and
A8: ( D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for Sd being Element of Fin (dom (App CFes)) st D2 = Sd holds
( M . (((M "**" (App CE1)) . s2),((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
( ( (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 A6, A1, A2, A3, A4, A5, Th126, Th40;
take D1 ; :: thesis: ex D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
take D2 ; :: thesis: ( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
thus ( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member ) by A7, A8; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let CE1, CE2 be FinSequence of D * ; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let f be FinSequence of D; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let d1, d2 be Element of D; :: thesis: ( len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E implies 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) )
assume A9: ( len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E ) ; :: thesis: 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let CFes be non-empty non empty FinSequence of D * ; :: thesis: ( CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees implies for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) )
assume A10: CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees ; :: thesis: for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let S1, S2 be Element of Fin (dom (App CFes)); :: thesis: ( S1 = D1 & S2 = D2 implies ( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) )
assume A11: ( S1 = D1 & S2 = D2 ) ; :: thesis: ( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
set fD = f ^ <*(A . (d1,d2))*>;
set fID = f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>;
A12: ( M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)) = A $$ (S1,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & i in dom h 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 A7, A9, A10, A11;
A13: ( M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)) = A $$ (S2,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S2 & i in dom h 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 A8, A9, A10, A11;
A14: ( len (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) = (len f) + 1 & len (f ^ <*(A . (d1,d2))*>) = (len f) + 1 ) by FINSEQ_2:16;
A15: ( card F = len E & len s1 = card F & card F = len s2 ) by A5, CARD_1:def 7;
CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m)))))) * Ees by A9, A10;
then len CFes = len Ees by CARD_1:def 7;
then A16: ( len CFes = (len Ee) + (len Es) & len Ee = len E & len E = len Es ) by A4, FINSEQ_1:22, A3, CARD_1:def 7;
A17: ( dom s1 = dom CE1 & dom s2 = dom CE2 ) by A15, A9, CARD_1:def 7, FINSEQ_3:29;
A18: ( s1 in doms CE1 & s2 in doms CE2 ) by A5, A14, A9, Th106;
thus S1 misses S2 :: thesis: ( A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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

assume S1 meets S2 ; :: thesis: contradiction
then consider x being object such that
A19: ( x in S1 & x in S2 ) by XBOOLE_0:3;
reconsider x = x as FinSequence by A19;
S1 c= dom (App CFes) by FINSUB_1:def 5;
then x in dom (App CFes) by A19;
then A20: len x = len CFes by Th47;
( len (s1 ^ s2) = (len s1) + (len s2) & (len s1) + (len s2) = len (s2 ^ s1) ) by FINSEQ_1:22;
then A21: ( dom (s1 ^ s2) = dom x & dom x = dom (s2 ^ s1) ) by A20, A16, A15, FINSEQ_3:30;
A22: dom s1 = dom s2 by A15, FINSEQ_3:29;
consider i being object such that
A23: ( i in dom s1 & s1 . i <> s2 . i ) by A5, A15, FINSEQ_3:29;
reconsider i = i as Nat by A23;
A24: ( (s1 ^ s2) . i = s1 . i & (s2 ^ s1) . i = s2 . i ) by A23, A22, FINSEQ_1:def 7;
A25: ( dom s1 c= dom (s1 ^ s2) & dom s2 c= dom (s2 ^ s1) ) by FINSEQ_1:26;
A26: ( 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 A17, A9, Th80, A23, A22;

per cases ( s1 . i = 1 + (len f) or s2 . i = 1 + (len f) or ( s1 . i <> 1 + (len f) & s2 . i <> 1 + (len f) ) ) ;

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

then x . i in {(1 + (len f)),(2 + (len f))} by A24, A21, A25, A7, A9, A10, A11, A19, A23;
then A28: ( x . i = 1 + (len f) or x . i = 2 + (len f) ) by TARSKI:def 2;
s2 . i in dom (CE2 . i) by A18, Th47, A23, A22;
then A29: s2 . i in dom (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) by A26, Def11;
x . i = s2 . i by A27, A21, A8, A9, A10, A11, A24, A25, A23, A19;
then (1 + (len f)) + 1 <= len (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) by FINSEQ_3:25, A29, A28, A27, A23;
hence contradiction by A14, NAT_1:13; :: thesis: verum

end;

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

then x . i in {(1 + (len f)),(2 + (len f))} by A23, A25, A21, A24, A19, A8, A9, A10, A11;
then A31: ( x . i = 1 + (len f) or x . i = 2 + (len f) ) by TARSKI:def 2;
s1 . i in dom (CE1 . i) by A18, Th47, A23;
then A32: s1 . i in dom (f ^ <*(A . (d1,d2))*>) by A26, Def11;
x . i = s1 . i by A23, A25, A21, A7, A9, A10, A11, A19, A30, A24;
then (1 + (len f)) + 1 <= len (f ^ <*(A . (d1,d2))*>) by FINSEQ_3:25, A32, A31, A30, A23;
hence contradiction by A14, NAT_1:13; :: thesis: verum

end;

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

then ( x . i = s1 . i & x . i = s2 . i ) by A21, A7, A9, A10, A11, A8, A24, A25, A23, A19;
hence contradiction by A23; :: thesis: verum

end;

end;

end;

hence A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) by A12, A13, A1, SETWOP_2:4; :: thesis: ( ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
thus for h being FinSequence
for i being Nat st h in S1 & 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 ) ) :: thesis: for h being FinSequence
for i being Nat st h in S2 & 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: for i being Nat st h in S1 & 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 ) )
let i be Nat; :: thesis: ( h in S1 & i in dom (s1 ^ s2) implies ( ( (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 ) ) )
assume A33: ( h in S1 & i in dom (s1 ^ s2) ) ; :: thesis: ( ( (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 ) )
S1 c= dom (App CFes) by FINSUB_1:def 5;
then h in dom (App CFes) by A33;
then A34: len h = len CFes by Th47;
len (s1 ^ s2) = len h by A34, A16, A15, FINSEQ_1:22;
then dom (s1 ^ s2) = dom h by FINSEQ_3:30;
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 A33, A7, A9, A10, A11; :: thesis: verum

end;

let h be FinSequence; :: thesis: for i being Nat st h in S2 & 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 ) )
let i be Nat; :: thesis: ( h in S2 & i in dom (s2 ^ s1) implies ( ( (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 ) ) )
assume A35: ( h in S2 & i in dom (s2 ^ s1) ) ; :: thesis: ( ( (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 ) )
S2 c= dom (App CFes) by FINSUB_1:def 5;
then h in dom (App CFes) by A35;
then len h = len CFes by Th47;
then len h = len (s2 ^ s1) by A16, A15, FINSEQ_1:22;
then dom h = dom (s2 ^ s1) by FINSEQ_3:30;
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 A35, A8, A9, A10, A11; :: thesis: verum

end;

suppose card (s1 " {(1 + m)}) < card (s2 " {(1 + m)}) ; :: thesis: ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )

hence ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 Th138, A1, A2, A3, A4, A5; :: thesis: verum

end;

suppose A36: card (s1 " {(1 + m)}) > card (s2 " {(1 + m)}) ; :: thesis: ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )

consider D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) such that
A37: ( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1))),(M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 Th138, A1, A2, A3, A4, A5, A36;
take D2 ; :: thesis: ex D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D2 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
take D1 ; :: thesis: ( D2 is with_evenly_repeated_values-member & D1 is with_evenly_repeated_values-member & ( 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) ) )
thus ( D2 is with_evenly_repeated_values-member & D1 is with_evenly_repeated_values-member ) by A37; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let CE1, CE2 be FinSequence of D * ; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let f be FinSequence of D; :: thesis: 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,F)) * E 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let d1, d2 be Element of D; :: thesis: ( len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E implies 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) )
assume A38: ( len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E ) ; :: thesis: 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 (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let CFes be non-empty non empty FinSequence of D * ; :: thesis: ( CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees implies for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) ) )
assume A39: CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees ; :: thesis: for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D2 & S2 = D1 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) )
let S2, S1 be Element of Fin (dom (App CFes)); :: thesis: ( S2 = D2 & S1 = D1 implies ( S2 misses S1 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S2 \/ S1),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) ) )
assume A40: ( S2 = D2 & S1 = D1 ) ; :: thesis: ( S2 misses S1 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S2 \/ S1),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S1 & 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 ) ) ) )
( len (f ^ <*(A . (d1,d2))*>) = m + 1 & m + 1 = len (f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>) ) by A38, FINSEQ_2:16;
then ( dom (App CE1) = doms ((m + 1),(card F)) & doms ((m + 1),(card F)) = dom (App CE2) ) by A38, Lm3;
then ( (M "**" (App CE1)) . s1 = M "**" ((App CE1) . s1) & (M "**" (App CE1)) . s2 = M "**" ((App CE1) . s2) & (M "**" (App CE2)) . s1 = M "**" ((App CE2) . s1) & (M "**" (App CE2)) . s2 = M "**" ((App CE2) . s2) ) by A5, Def10;
then reconsider m11 = (M "**" (App CE1)) . s1, m21 = (M "**" (App CE2)) . s1, m22 = (M "**" (App CE2)) . s2, m12 = (M "**" (App CE1)) . s2 as Element of D ;
A $$ ((S1 \/ S2),(M "**" (App CFes))) = A . ((M . (m12,m21)),(M . (m11,m22))) by A37, A38, A39, A40
.= A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) by A1, BINOP_1:def 2 ;
hence ( S2 misses S1 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S2 \/ S1),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S2 & 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 ) ) ) & ( for h being FinSequence
for i being Nat st h in S1 & 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 A37, A38, A39, A40; :: thesis: verum

end;

end;