let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
let B be BinOp of D; :: thesis: for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
let f be FinSequence of D; :: thesis: for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
let F1, F2 be finite set ; :: thesis: for E1 being Enumeration of F1
for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
set C1 = SignGenOp (f,B,F1);
set C2 = SignGenOp (f,B,F2);
set C12 = SignGenOp (f,B,(F1 \/ F2));
let E1 be Enumeration of F1; :: thesis: for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
let E2 be Enumeration of F2; :: thesis: for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
let E12 be Enumeration of F1 \/ F2; :: thesis: ( E12 = E1 ^ E2 implies (SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2) )
assume A1: E12 = E1 ^ E2 ; :: thesis: (SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)
A2: ( len ((SignGenOp (f,B,F1)) * E1) = len E1 & len E1 = card F1 & len ((SignGenOp (f,B,F2)) * E2) = len E2 & len E2 = card F2 & len ((SignGenOp (f,B,(F1 \/ F2))) * E12) = len E12 & len E12 = card (F1 \/ F2) ) by CARD_1:def 7;
( F1 = rng E1 & rng E1 misses rng E2 & rng E2 = F2 ) by A1, FINSEQ_3:91, RLAFFIN3:def 1;
then A3: card (F1 \/ F2) = (card F1) + (card F2) by CARD_2:40;
A4: len ((SignGenOp (f,B,(F1 \/ F2))) * E12) = len (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) by A2, A3, FINSEQ_1:22;
A5: ( dom E1 = dom ((SignGenOp (f,B,F1)) * E1) & dom E2 = dom ((SignGenOp (f,B,F2)) * E2) ) by A2, FINSEQ_3:30;
for k being Nat st 1 <= k & k <= len ((SignGenOp (f,B,(F1 \/ F2))) * E12) holds
((SignGenOp (f,B,(F1 \/ F2))) * E12) . k = (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((SignGenOp (f,B,(F1 \/ F2))) * E12) implies ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k = (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k )
assume A6: ( 1 <= k & k <= len ((SignGenOp (f,B,(F1 \/ F2))) * E12) ) ; :: thesis: ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k = (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k
A7: k in dom ((SignGenOp (f,B,(F1 \/ F2))) * E12) by A6, FINSEQ_3:25;
k in dom (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) by A6, A4, FINSEQ_3:25;

per cases then ( k in dom ((SignGenOp (f,B,F1)) * E1) or ex i being Nat st
( i in dom ((SignGenOp (f,B,F2)) * E2) & k = (len ((SignGenOp (f,B,F1)) * E1)) + i ) ) by FINSEQ_1:25;

suppose A8: k in dom ((SignGenOp (f,B,F1)) * E1) ; :: thesis: ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k = (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k

hence (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k = ((SignGenOp (f,B,F1)) * E1) . k by FINSEQ_1:def 7
.= SignGen (f,B,(E1 . k)) by A8, Th80
.= SignGen (f,B,(E12 . k)) by A1, A8, A5, FINSEQ_1:def 7
.= ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k by A7, Th80 ;
:: thesis: verum

end;

suppose ex i being Nat st
( i in dom ((SignGenOp (f,B,F2)) * E2) & k = (len ((SignGenOp (f,B,F1)) * E1)) + i ) ; :: thesis: ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k = (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k

then consider i being Nat such that
A9: ( i in dom ((SignGenOp (f,B,F2)) * E2) & k = (len ((SignGenOp (f,B,F1)) * E1)) + i ) ;
thus (((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)) . k = ((SignGenOp (f,B,F2)) * E2) . i by A9, FINSEQ_1:def 7
.= SignGen (f,B,(E2 . i)) by A9, Th80
.= SignGen (f,B,(E12 . k)) by A1, A9, A5, A2, FINSEQ_1:def 7
.= ((SignGenOp (f,B,(F1 \/ F2))) * E12) . k by A7, Th80 ; :: thesis: verum

end;

end;

end;

hence (SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2) by A2, A3, FINSEQ_1:22; :: thesis: verum