let L be non empty left_zeroed add-associative doubleLoopStr ; :: thesis: for B1, B2 being bag of the carrier of L
for E being the carrier of L -valued FinSequence holds (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)
let B1, B2 be bag of the carrier of L; :: thesis: for E being the carrier of L -valued FinSequence holds (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)
let E be the carrier of L -valued FinSequence; :: thesis: (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)
A1: len (B1 (++) E) = len E by Def1;
A2: len (B2 (++) E) = len E by Def1;
A3: len ((B1 + B2) (++) E) = len E by Def1;
hence A4: len ((B1 + B2) (++) E) = len ((B1 (++) E) + (B2 (++) E)) by A1, A2, MATRIX14:2; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((B1 + B2) (++) E) or ((B1 + B2) (++) E) . b₁ = ((B1 (++) E) + (B2 (++) E)) . b₁ )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len ((B1 + B2) (++) E) or ((B1 + B2) (++) E) . n = ((B1 (++) E) + (B2 (++) E)) . n )
assume A5: ( 1 <= n & n <= len ((B1 + B2) (++) E) ) ; :: thesis: ((B1 + B2) (++) E) . n = ((B1 (++) E) + (B2 (++) E)) . n
then A6: n in dom ((B1 (++) E) + (B2 (++) E)) by A4, FINSEQ_3:25;
A7: n in dom E by A3, A5, FINSEQ_3:25;
dom (B1 (++) E) = dom (B2 (++) E) by A1, A2, FINSEQ_3:29;
then A8: ( (B1 (++) E) . n = (B1 (++) E) /. n & (B2 (++) E) . n = (B2 (++) E) /. n ) by A1, A3, A5, FINSEQ_3:25, PARTFUN1:def 6;
A9: (B1 (++) E) . n = ((B1 * E) . n) * (E /. n) by A1, A3, A5, Def1;
A10: (B2 (++) E) . n = ((B2 * E) . n) * (E /. n) by A2, A3, A5, Def1;
A11: ( (B1 * E) . n = B1 . (E . n) & (B2 * E) . n = B2 . (E . n) ) by A7, FUNCT_1:13;
A12: ((B1 + B2) * E) . n = (B1 + B2) . (E . n) by A7, FUNCT_1:13
.= (B1 . (E . n)) + (B2 . (E . n)) by PRE_POLY:def 5 ;
thus ((B1 + B2) (++) E) . n = (((B1 + B2) * E) . n) * (E /. n) by A5, Def1
.= ((B1 (++) E) /. n) + ((B2 (++) E) /. n) by A8, A9, A10, A11, A12, BINOM:15
.= ((B1 (++) E) + (B2 (++) E)) . n by A6, A8, FVSUM_1:17 ; :: thesis: verum