let K be non empty multMagma ; :: thesis: for f, g being FinSequence of K
for a being Element of K holds a * (f ^ g) = (a * f) ^ (a * g)
let f, g be FinSequence of K; :: thesis: for a being Element of K holds a * (f ^ g) = (a * f) ^ (a * g)
let a be Element of K; :: thesis: a * (f ^ g) = (a * f) ^ (a * g)
set KK = the carrier of K;
reconsider F = f as Element of (len f) -tuples_on the carrier of K by FINSEQ_2:92;
reconsider G = g as Element of (len g) -tuples_on the carrier of K by FINSEQ_2:92;
reconsider FG = F ^ G, aFaG = (a * F) ^ (a * G) as Element of ((len f) + (len g)) -tuples_on the carrier of K by FINSEQ_2:131;

now :: thesis: for i being Nat st i in Seg ((len f) + (len g)) holds
(a * FG) . i = aFaG . i

let i be Nat; :: thesis: ( i in Seg ((len f) + (len g)) implies (a * FG) . i = aFaG . i )
assume A1: i in Seg ((len f) + (len g)) ; :: thesis: (a * FG) . i = aFaG . i
A2: i in dom FG by A1, FINSEQ_2:124;

now :: thesis: (a * FG) . i = aFaG . i

per cases ( i in dom f or ex n being Nat st
( n in dom g & i = (len f) + n ) ) by A2, FINSEQ_1:25;

suppose A3: i in dom f ; :: thesis: (a * FG) . i = aFaG . i

A4: rng f c= the carrier of K by RELAT_1:def 19;
f . i in rng f by A3, FUNCT_1:def 3;
then reconsider fi = f . i as Element of K by A4;
A5: dom F = Seg (len f) by FINSEQ_2:124;
A6: dom (a * F) = Seg (len f) by FINSEQ_2:124;
FG . i = fi by A3, FINSEQ_1:def 7;
hence (a * FG) . i = a * fi by A1, FVSUM_1:51
.= (a * F) . i by A3, A5, FVSUM_1:51
.= aFaG . i by A3, A5, A6, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A7: ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: (a * FG) . i = aFaG . i

A8: rng g c= the carrier of K by RELAT_1:def 19;
A9: ( dom (a * G) = Seg (len g) & len (a * F) = len f ) by CARD_1:def 7, FINSEQ_2:124;
consider n being Nat such that
A10: n in dom g and
A11: i = (len f) + n by A7;
g . n in rng g by A10, FUNCT_1:def 3;
then reconsider gn = g . n as Element of K by A8;
A12: dom G = Seg (len g) by FINSEQ_2:124;
FG . i = gn by A10, A11, FINSEQ_1:def 7;
hence (a * FG) . i = a * gn by A1, FVSUM_1:51
.= (a * G) . n by A10, A12, FVSUM_1:51
.= aFaG . i by A10, A11, A12, A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (a * FG) . i = aFaG . i ; :: thesis: verum

end;

hence a * (f ^ g) = (a * f) ^ (a * g) by FINSEQ_2:119; :: thesis: verum