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;

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

hence
a * (f ^ g) = (a * f) ^ (a * g)
by FINSEQ_2:119; :: thesis: verum(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;

end;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 . iend;

hence
(a * FG) . i = aFaG . i
; :: thesis: verumper cases
( i in dom f or ex n being Nat st

( n in dom g & i = (len f) + n ) ) by A2, FINSEQ_1:25;

end;

( 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;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

suppose A7:
ex n being Nat st

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

( 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;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