let D be non empty set ; for A, M being BinOp of D
for d1, d2 being Element of D
for F1, F2 being finite set st M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let A, M be BinOp of D; for d1, d2 being Element of D
for F1, F2 being finite set st M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let d1, d2 be Element of D; for F1, F2 being finite set st M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let F1, F2 be finite set ; ( M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A implies for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2)) )
set I = the_inverseOp_wrt A;
assume that
A1:
( M is commutative & M is associative & M is having_a_unity )
and
A2:
( A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp )
and
A3:
M is_distributive_wrt A
; for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let f be FinSequence of D; for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let E1 be Enumeration of F1; for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
let E2 be Enumeration of F2; for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
set L = 1 + (len f);
let s1, s2 be FinSequence; ( s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) implies M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2)) )
assume A4:
( s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) )
; M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
A5:
( len (f ^ <*d1*>) = 1 + (len f) & 1 + (len f) = len (f ^ <*d2*>) )
by FINSEQ_2:16;
then A6:
( doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) = doms ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1) & doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) = doms ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2) )
by Th107;
set k = card (s1 " {(1 + (len f))});
A7:
( len s1 = len ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & len ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) = len E1 & len s2 = len ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & len ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) = len E2 )
by Th47, A4, CARD_1:def 7;
then A8:
( dom s1 = dom E1 & dom s2 = dom E2 )
by FINSEQ_3:29;
set kL = (card (s1 " {(1 + (len f))})) |-> (1 + (len f));
A9:
len ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = card (s1 " {(1 + (len f))})
;
consider p1 being Permutation of (dom s1), S1 being FinSequence such that
A10:
( s1 * p1 = S1 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) & not 1 + (len f) in rng S1 )
by Th134;
reconsider E1p = E1 * p1 as Enumeration of F1 by A8, Th109;
A11:
( len E1p = card F1 & card F1 = len E1 )
by CARD_1:def 7;
( dom p1 = dom s1 & dom s1 = rng p1 )
by FUNCT_2:52, FUNCT_2:def 3;
then A12:
( (len S1) + (card (s1 " {(1 + (len f))})) = len (S1 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) & len (S1 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = len s1 )
by A10, FINSEQ_3:29, A9, FINSEQ_1:22, RELAT_1:27;
set e1pS = E1p | (len S1);
consider e1pK being FinSequence such that
A13:
E1p = (E1p | (len S1)) ^ e1pK
by FINSEQ_1:80;
set F1S = rng (E1p | (len S1));
set F1K = rng e1pK;
A14:
len (E1p | (len S1)) = len S1
by NAT_1:11, A7, A11, A12, FINSEQ_1:59;
A15:
len E1p = (len (E1p | (len S1))) + (len e1pK)
by A13, FINSEQ_1:22;
A16:
( E1p | (len S1) is one-to-one & e1pK is one-to-one & rng (E1p | (len S1)) misses rng e1pK )
by A13, FINSEQ_3:91;
then reconsider E1pS = E1p | (len S1) as Enumeration of rng (E1p | (len S1)) by RLAFFIN3:def 1;
reconsider E1pK = e1pK as Enumeration of rng e1pK by A16, RLAFFIN3:def 1;
consider p2 being Permutation of (dom s2), S2 being FinSequence such that
A17:
( s2 * p2 = S2 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) & not 1 + (len f) in rng S2 )
by A4, Th134;
reconsider E2p = E2 * p2 as Enumeration of F2 by A8, Th109;
A18:
( len E2p = card F2 & card F2 = len E2 )
by CARD_1:def 7;
( dom p2 = dom s2 & dom s2 = rng p2 )
by FUNCT_2:52, FUNCT_2:def 3;
then A19:
( (len S2) + (card (s1 " {(1 + (len f))})) = len (S2 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) & len (S2 ^ ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = len s2 )
by A17, FINSEQ_3:29, A9, FINSEQ_1:22, RELAT_1:27;
set e2pS = E2p | (len S2);
A20:
len (E2p | (len S2)) = len S2
by NAT_1:11, A7, A18, A19, FINSEQ_1:59;
consider e2pK being FinSequence such that
A21:
E2p = (E2p | (len S2)) ^ e2pK
by FINSEQ_1:80;
set F2S = rng (E2p | (len S2));
set F2K = rng e2pK;
A22:
len E2p = (len (E2p | (len S2))) + (len e2pK)
by A21, FINSEQ_1:22;
A23:
( E2p | (len S2) is one-to-one & e2pK is one-to-one & rng (E2p | (len S2)) misses rng e2pK )
by A21, FINSEQ_3:91;
then reconsider E2pS = E2p | (len S2) as Enumeration of rng (E2p | (len S2)) by RLAFFIN3:def 1;
reconsider E2pK = e2pK as Enumeration of rng e2pK by A23, RLAFFIN3:def 1;
A24:
( F1 = rng E1p & rng E1p = (rng (E1p | (len S1))) \/ (rng e1pK) & F2 = rng E2p & rng E2p = (rng (E2p | (len S2))) \/ (rng e2pK) )
by A13, A21, FINSEQ_1:31, RLAFFIN3:def 1;
then A25:
( (SignGenOp ((f ^ <*d1*>),A,F1)) * E1p = ((SignGenOp ((f ^ <*d1*>),A,(rng (E1p | (len S1))))) * E1pS) ^ ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK) & (SignGenOp ((f ^ <*d2*>),A,F2)) * E2p = ((SignGenOp ((f ^ <*d2*>),A,(rng (E2p | (len S2))))) * E2pS) ^ ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK) )
by A13, A21, Th81;
A26:
( (SignGenOp ((f ^ <*d2*>),A,F1)) * E1p = ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS) ^ ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK) & (SignGenOp ((f ^ <*d1*>),A,F2)) * E2p = ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS) ^ ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK) )
by A13, A21, Th81, A24;
A27:
( s1 * p1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1p) & s2 * p2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p) )
by A4, A8, Th110;
then A28:
( s1 * p1 in dom (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1p)) & s2 * p2 in dom (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p)) )
by Def9;
A29:
( s1 * p1 in doms ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1p) & s2 * p2 in doms ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p) )
by A4, A8, Th110, A6;
then A30:
( s1 * p1 in dom (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1p)) & s2 * p2 in dom (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p)) )
by Def9;
len ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK) = len ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))
by A15, A7, A11, A14, A12, CARD_1:def 7;
then A31:
( S1 in doms ((SignGenOp ((f ^ <*d1*>),A,(rng (E1p | (len S1))))) * E1pS) & (card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in doms ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK) )
by A27, Th50, A10, A25;
len ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK) = len ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))
by A15, A7, A11, A14, A12, CARD_1:def 7;
then A32:
( S1 in doms ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS) & (card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in doms ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK) )
by A29, Th50, A10, A26;
s2 * p2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p)
by A4, A8, Th110;
then A33:
s2 * p2 in dom (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p))
by Def9;
len ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK) = len ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))
by A22, A7, A20, A19, A18, CARD_1:def 7;
then A34:
( S2 in doms ((SignGenOp ((f ^ <*d2*>),A,(rng (E2p | (len S2))))) * E2pS) & (card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in doms ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK) )
by A27, Th50, A17, A25;
s2 * p2 in doms ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p)
by A6, A4, A8, Th110;
then A35:
s2 * p2 in dom (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p))
by Def9;
len ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK) = len ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))
by A22, A7, A20, A19, A18, CARD_1:def 7;
then A36:
( S2 in doms ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS) & (card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in doms ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK) )
by A29, Th50, A17, A26;
A37: (M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1 =
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1p))) . (s1 * p1)
by A1, A4, A8, Th112
.=
M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1p)) . (s1 * p1))
by A28, Def10
.=
M "**" (((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1) ^ ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))
by Th61, A25, A10, A31
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A1, FINSOP_1:5
;
A38: (M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2 =
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p))) . (s2 * p2)
by A1, A4, A8, Th112
.=
M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2p)) . (s2 * p2))
by A33, Def10
.=
M "**" (((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2) ^ ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))
by Th61, A25, A17, A34
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A1, FINSOP_1:5
;
A39:
(App ((SignGenOp ((f ^ <*d2*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2 = (App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2
by A17, A34, Th133;
A40:
(App ((SignGenOp ((f ^ <*d1*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1 = (App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1
by Th133, A32, A10;
A41:
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
proof
defpred S1[
object ]
means 1
+ (len f) in E1pK . $1;
consider D1 being
set such that A42:
for
x being
object holds
(
x in D1 iff (
x in dom E1pK &
S1[
x] ) )
from XBOOLE_0:sch 1();
D1 c= dom E1pK
by A42;
then reconsider D1 =
D1 as
Subset of
(dom E1pK) ;
A43:
for
i being
Nat holds
(
i in D1 iff 1
+ (len f) in E1pK . i )
defpred S2[
object ]
means 1
+ (len f) in E2pK . $1;
consider D2 being
set such that A45:
for
x being
object holds
(
x in D2 iff (
x in dom E2pK &
S2[
x] ) )
from XBOOLE_0:sch 1();
D2 c= dom E2pK
by A45;
then reconsider D2 =
D2 as
Subset of
(dom E2pK) ;
A46:
for
i being
Nat holds
(
i in D2 iff 1
+ (len f) in E2pK . i )
1
<= 1
+ (len f)
by NAT_1:11;
then A48:
( 1
+ (len f) in dom (f ^ <*d1*>) & 1
+ (len f) in dom (f ^ <*d2*>) )
by A5, FINSEQ_3:25;
then A49:
(
(f ^ <*d1*>) /. (1 + (len f)) = (f ^ <*d1*>) . (1 + (len f)) &
(f ^ <*d1*>) . (1 + (len f)) = d1 &
(f ^ <*d2*>) /. (1 + (len f)) = (f ^ <*d2*>) . (1 + (len f)) &
(f ^ <*d2*>) . (1 + (len f)) = d2 )
by PARTFUN1:def 6;
(
(card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in dom (App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) &
(card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in dom (App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) &
(card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in dom (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) &
(card (s1 " {(1 + (len f))})) |-> (1 + (len f)) in dom (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) )
by Def9, A31, A32, A34, A36;
then A50:
(
M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = (M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) &
M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = (M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) &
M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = (M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) &
M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))) = (M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) )
by Def10;
per cases
( card D1 is even or not card D1 is even )
;
suppose
card D1 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then A51:
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d1) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d2) )
by A49, A15, A7, A11, A14, A12, Th135, A48, A43, A1, A2, A3;
per cases
( card D2 is even or not card D2 is even )
;
suppose
card D2 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d1) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d2) )
by A49, A22, A7, A20, A19, A18, Th135, A48, A46, A1, A2, A3;
hence
M . (
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
= M . (
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A51, A50, A1, BINOP_1:def 2;
verum end; suppose
not
card D2 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then A52:
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d1)) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d2)) )
by A49, A22, A7, A20, A19, A18, Th135, A48, A46, A1, A2, A3;
hence M . (
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) =
M . (
((the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d2))),
(M "**" ((card (s1 " {(1 + (len f))})) |-> d1)))
by A51, A50, A1, BINOP_1:def 2
.=
(the_inverseOp_wrt A) . (M . ((M "**" ((card (s1 " {(1 + (len f))})) |-> d2)),(M "**" ((card (s1 " {(1 + (len f))})) |-> d1))))
by A2, A3, FINSEQOP:67
.=
M . (
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A51, A52, A50, A2, A3, FINSEQOP:67
;
verum end; end; suppose
not
card D1 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then A53:
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d1)) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d2)) )
by A49, A15, A7, A11, A14, A12, Th135, A48, A43, A1, A2, A3;
per cases
( card D2 is even or not card D2 is even )
;
suppose
card D2 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then A54:
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d1) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = M "**" ((card (s1 " {(1 + (len f))})) |-> d2) )
by A49, A22, A7, A20, A19, A18, Th135, A48, A46, A1, A2, A3;
hence M . (
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) =
M . (
(M "**" ((card (s1 " {(1 + (len f))})) |-> d2)),
((the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d1))))
by A53, A50, A1, BINOP_1:def 2
.=
(the_inverseOp_wrt A) . (M . ((M "**" ((card (s1 " {(1 + (len f))})) |-> d2)),(M "**" ((card (s1 " {(1 + (len f))})) |-> d1))))
by A2, A3, FINSEQOP:67
.=
M . (
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A53, A54, A50, A2, A3, FINSEQOP:67
;
verum end; suppose
not
card D2 is
even
;
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))) = M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))then
(
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d1)) &
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK))) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))) = (the_inverseOp_wrt A) . (M "**" ((card (s1 " {(1 + (len f))})) |-> d2)) )
by A49, A22, A7, A20, A19, A18, Th135, A48, A46, A1, A2, A3;
hence
M . (
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
= M . (
(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),
(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A53, A50, A1, BINOP_1:def 2;
verum end; end;
end;
A55: (M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1 =
(M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1p))) . (s1 * p1)
by A1, A4, A8, Th112, A6
.=
M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1p)) . (s1 * p1))
by A30, Def10
.=
M "**" (((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1) ^ ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))
by Th61, A26, A10, A32
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A1, FINSOP_1:5
;
A56: (M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2 =
(M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p))) . (s2 * p2)
by A1, A4, A8, Th112, A6
.=
M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2p)) . (s2 * p2))
by A35, Def10
.=
M "**" (((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2) ^ ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f)))))
by Th61, A26, A17, A36
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))
by A1, FINSOP_1:5
;
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) =
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))))))
by A37, A38, A39, A40, A1, BINOP_1:def 3
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)))))))
by A1, BINOP_1:def 2
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M . ((M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)))))
by A1, BINOP_1:def 3
.=
M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)))))))
by A41, A1, BINOP_1:def 3
.=
M . ((M . ((M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng (E1p | (len S1))))) * E1pS)) . S1)),(M "**" ((App ((SignGenOp ((f ^ <*d2*>),A,(rng e1pK))) * E1pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))))),(M . ((M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng e2pK))) * E2pK)) . ((card (s1 " {(1 + (len f))})) |-> (1 + (len f))))),(M "**" ((App ((SignGenOp ((f ^ <*d1*>),A,(rng (E2p | (len S2))))) * E2pS)) . S2)))))
by A1, BINOP_1:def 3
.=
M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
by A55, A56, A1, BINOP_1:def 2
;
hence
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))
; verum