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:110;
reconsider G = g as Element of (len g) -tuples_on the carrier of K by FINSEQ_2:110;
reconsider FG = F ^ G, aFaG = (a * F) ^ (a * G) as Element of ((len f) + (len g)) -tuples_on the carrier of K ;

now

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:144;

now

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

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

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

end;

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

then consider n being Nat such that
A5: ( n in dom g & i = (len f) + n ) ;
A6: ( dom G = Seg (len g) & dom (a * G) = Seg (len g) & len (a * F) = len f ) by FINSEQ_1:def 18, FINSEQ_2:144;
( g . n in rng g & rng g c= the carrier of K ) by A5, FUNCT_1:def 5, RELAT_1:def 19;
then reconsider gn = g . n as Element of K ;
FG . i = gn by A5, FINSEQ_1:def 7;
hence (a * FG) . i = a * gn by A1, FVSUM_1:63
.= (a * G) . n by A5, A6, FVSUM_1:63
.= aFaG . i by A5, A6, 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:139; :: thesis: verum