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 ;
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 ;
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 ;
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 ;
hence (a * FG) . i = a * fi by
.= (a * F) . i by
.= aFaG . i by ;
:: 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 ;
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 ;
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 ;
hence (a * FG) . i = a * gn by
.= (a * G) . n by
.= aFaG . i by ;
:: 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