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;

(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

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

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

hence
(FH + GW) . i = Th36W . i
; :: thesis: verumper cases
( i in dom f or ex n being Nat st

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

end;

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

suppose
ex n being Nat st

( n in dom h & i = (len f) + n ) ; :: thesis: (FH + GW) . i = Th36W . i

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