let K be non empty addLoopStr ; :: thesis: for f, g, h, w being FinSequence of K st len f = len g & len h = len w holds
(f ^ h) + (g ^ w) = (f + g) ^ (h + w)
let f, g, h, w be FinSequence of K; :: thesis: ( len f = len g & len h = len w implies (f ^ h) + (g ^ w) = (f + g) ^ (h + w) )
assume A1: ( len f = len g & len h = len w ) ; :: thesis: (f ^ h) + (g ^ w) = (f + g) ^ (h + w)
set KK = the carrier of K;
reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by A1, FINSEQ_2:110;
reconsider H = h, W = w as Element of (len h) -tuples_on the carrier of K by A1, FINSEQ_2:110;
reconsider FH = F ^ H, GW = G ^ W, Th36W = (F + G) ^ (H + W) as Element of ((len f) + (len h)) -tuples_on the carrier of K ;

now

let i be Nat; :: thesis: ( i in Seg ((len f) + (len h)) implies (FH + GW) . i = Th36W . i )
assume A2: i in Seg ((len f) + (len h)) ; :: thesis: (FH + GW) . i = Th36W . i
A3: i in dom FH by A2, FINSEQ_2:144;

now

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

suppose A4: i in dom f ; :: thesis: (FH + GW) . i = Th36W . i

A5: ( dom F = Seg (len f) & dom G = Seg (len f) & dom (F + G) = Seg (len f) ) by FINSEQ_2:144;
then ( f . i in rng f & rng f c= the carrier of K & g . i in rng g & rng g c= the carrier of K ) by A4, FUNCT_1:def 5, RELAT_1:def 19;
then reconsider fi = f . i, gi = g . i as Element of K ;
( FH . i = fi & GW . i = gi ) by A4, A5, FINSEQ_1:def 7;
hence (FH + GW) . i = fi + gi by A2, FVSUM_1:22
.= (F + G) . i by A4, A5, FVSUM_1:22
.= Th36W . i by A4, A5, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom h & i = (len f) + n ) ; :: thesis: (FH + GW) . i = Th36W . i

then consider n being Nat such that
A6: ( n in dom h & i = (len f) + n ) ;
A7: ( dom H = Seg (len h) & dom W = Seg (len h) & dom (H + W) = Seg (len h) & len (F + G) = len f ) by FINSEQ_1:def 18, FINSEQ_2:144;
then ( h . n in rng h & rng h c= the carrier of K & w . n in rng w & rng w c= the carrier of K ) by A6, FUNCT_1:def 5, RELAT_1:def 19;
then reconsider hn = h . n, wn = w . n as Element of K ;
( FH . i = hn & GW . i = wn ) by A1, A6, A7, FINSEQ_1:def 7;
hence (FH + GW) . i = hn + wn by A2, FVSUM_1:22
.= (H + W) . n by A6, A7, FVSUM_1:22
.= Th36W . i by A6, A7, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (FH + GW) . i = Th36W . i ; :: thesis: verum

end;

hence (f ^ h) + (g ^ w) = (f + g) ^ (h + w) by FINSEQ_2:139; :: thesis: verum