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 that
A1: len f = len g and
A2: len h = len w ; :: thesis: (f ^ h) + (g ^ w) = (f + g) ^ (h + w)
set KK = the carrier of K;
reconsider H = h, W = w as Element of (len h) -tuples_on the carrier of K by A2, FINSEQ_2:92;
reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by A1, FINSEQ_2:92;
reconsider FH = F ^ H, GW = G ^ W, Th36W = (F + G) ^ (H + W) as Tuple of (len f) + (len h), the carrier of K ;
reconsider FH = FH, GW = GW, Th36W = Th36W as Element of ((len f) + (len h)) -tuples_on the carrier of K by FINSEQ_2:131;

now :: thesis: for i being Nat st i in Seg ((len f) + (len h)) holds
(FH + GW) . i = Th36W . i

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

now :: thesis: (FH + GW) . i = Th36W . i

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

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

A6: ( rng f c= the carrier of K & rng g c= the carrier of K ) by RELAT_1:def 19;
A7: dom (F + G) = Seg (len f) by FINSEQ_2:124;
A8: f . i in rng f by A5, FUNCT_1:def 3;
A9: dom F = Seg (len f) by FINSEQ_2:124;
A10: dom G = Seg (len f) by FINSEQ_2:124;
then g . i in rng g by A5, A9, FUNCT_1:def 3;
then reconsider fi = f . i, gi = g . i as Element of K by A8, A6;
A11: FH . i = fi by A5, FINSEQ_1:def 7;
GW . i = gi by A5, A9, A10, FINSEQ_1:def 7;
hence (FH + GW) . i = fi + gi by A3, A11, FVSUM_1:18
.= (F + G) . i by A5, A9, FVSUM_1:18
.= Th36W . i by A5, A9, A7, 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
A12: n in dom h and
A13: i = (len f) + n ;
A14: h . n in rng h by A12, FUNCT_1:def 3;
A15: ( rng h c= the carrier of K & rng w c= the carrier of K ) by RELAT_1:def 19;
A16: dom H = Seg (len h) by FINSEQ_2:124;
A17: dom W = Seg (len h) by FINSEQ_2:124;
then w . n in rng w by A12, A16, FUNCT_1:def 3;
then reconsider hn = h . n, wn = w . n as Element of K by A14, A15;
A18: FH . i = hn by A12, A13, FINSEQ_1:def 7;
A19: ( dom (H + W) = Seg (len h) & len (F + G) = len f ) by CARD_1:def 7, FINSEQ_2:124;
GW . i = wn by A1, A12, A13, A16, A17, FINSEQ_1:def 7;
hence (FH + GW) . i = hn + wn by A3, A18, FVSUM_1:18
.= (H + W) . n by A12, A16, FVSUM_1:18
.= Th36W . i by A12, A13, A16, A19, 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:119; :: thesis: verum