let L be non empty left_zeroed add-associative doubleLoopStr ; :: thesis: for B being bag of the carrier of L
for E, F being the carrier of L -valued FinSequence holds B (++) (E ^ F) = (B (++) E) ^ (B (++) F)
let B be bag of the carrier of L; :: thesis: for E, F being the carrier of L -valued FinSequence holds B (++) (E ^ F) = (B (++) E) ^ (B (++) F)
let E, F be the carrier of L -valued FinSequence; :: thesis: B (++) (E ^ F) = (B (++) E) ^ (B (++) F)
A1: len (B (++) (E ^ F)) = len (E ^ F) by Def1;
A2: len (B (++) E) = len E by Def1;
A3: len (B (++) F) = len F by Def1;
A4: (len (B (++) E)) + (len (B (++) F)) = len ((B (++) E) ^ (B (++) F)) by FINSEQ_1:22;
A5: len (E ^ F) = (len E) + (len F) by FINSEQ_1:22;
then A6: len (B (++) (E ^ F)) = (len (B (++) E)) + (len (B (++) F)) by A2, A3, Def1;
hence len (B (++) (E ^ F)) = len ((B (++) E) ^ (B (++) F)) by FINSEQ_1:22; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (B (++) (E ^ F)) or (B (++) (E ^ F)) . b₁ = ((B (++) E) ^ (B (++) F)) . b₁ )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len (B (++) (E ^ F)) or (B (++) (E ^ F)) . n = ((B (++) E) ^ (B (++) F)) . n )
assume that
A7: 1 <= n and
A8: n <= len (B (++) (E ^ F)) ; :: thesis: (B (++) (E ^ F)) . n = ((B (++) E) ^ (B (++) F)) . n
A9: (B (++) (E ^ F)) . n = ((B * (E ^ F)) . n) * ((E ^ F) /. n) by A7, A8, Def1;
A10: n in dom (E ^ F) by A1, A7, A8, FINSEQ_3:25;
then A11: (B * (E ^ F)) . n = B . ((E ^ F) . n) by FUNCT_1:13;
A12: ( E is FinSequence of L & F is FinSequence of L ) by NEWTON02:103;
A13: (E ^ F) . n = (E ^ F) /. n by A10, PARTFUN1:def 6;

per cases ( n <= len E or n > len E ) ;

suppose A14: n <= len E ; :: thesis: (B (++) (E ^ F)) . n = ((B (++) E) ^ (B (++) F)) . n

then A15: n in dom E by A7, FINSEQ_3:25;
A16: (E ^ F) . n = E . n by A7, A14, FINSEQ_1:64;
A17: (E ^ F) /. n = E /. n by A15, A12, FINSEQ_4:68;
(B * E) . n = B . (E . n) by A15, FUNCT_1:13;
hence (B (++) (E ^ F)) . n = (B (++) E) . n by A2, A7, A14, A9, A11, A16, A17, Def1
.= ((B (++) E) ^ (B (++) F)) . n by A2, A7, A14, FINSEQ_1:64 ;
:: thesis: verum

end;

suppose A18: n > len E ; :: thesis: (B (++) (E ^ F)) . n = ((B (++) E) ^ (B (++) F)) . n

then A19: (E ^ F) . n = F . (n - (len E)) by A1, A8, FINSEQ_1:24;
set m = n - (len (B (++) E));
A20: n - (len (B (++) E)) in NAT by A2, A18, INT_1:5;
n - n < n - (len E) by A18, XREAL_1:15;
then A21: 0 + 1 <= n - (len (B (++) E)) by A2, A20, NAT_1:13;
A22: n - (len E) <= ((len E) + (len F)) - (len E) by A1, A8, A5, XREAL_1:9;
then A23: n - (len (B (++) E)) in dom F by A2, A20, A21, FINSEQ_3:25;
then A24: (B * F) . (n - (len (B (++) E))) = B . (F . (n - (len (B (++) E)))) by FUNCT_1:13;
F /. (n - (len (B (++) E))) = F . (n - (len (B (++) E))) by A23, PARTFUN1:def 6;
hence (B (++) (E ^ F)) . n = (B (++) F) . (n - (len (B (++) E))) by A3, A20, A21, A22, A2, A13, A24, A19, A11, A9, Def1
.= ((B (++) E) ^ (B (++) F)) . n by A2, A6, A4, A8, A18, FINSEQ_1:24 ;
:: thesis: verum

end;

end;