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 ;
reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by ;
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 ;
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 ;
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 ;
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 ;
then reconsider fi = f . i, gi = g . i as Element of K by A8, A6;
A11: FH . i = fi by ;
GW . i = gi by ;
hence (FH + GW) . i = fi + gi by
.= (F + G) . i by
.= Th36W . i by ;
:: 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 ;
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 ;
then reconsider hn = h . n, wn = w . n as Element of K by ;
A18: FH . i = hn by ;
A19: ( dom (H + W) = Seg (len h) & len (F + G) = len f ) by ;
GW . i = wn by ;
hence (FH + GW) . i = hn + wn by
.= (H + W) . n by
.= Th36W . i by ;
:: 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