let D be non empty set ; :: thesis: for i being Nat
for f, g being FinSequence of D * st i in dom ((D -concatenation) "**" f) holds
( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) )
let i be Nat; :: thesis: for f, g being FinSequence of D * st i in dom ((D -concatenation) "**" f) holds
( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) )
let f, g be FinSequence of D * ; :: thesis: ( i in dom ((D -concatenation) "**" f) implies ( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) ) )
set DC = D -concatenation ;
assume A1: i in dom ((D -concatenation) "**" f) ; :: thesis: ( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) )
A2: (D -concatenation) "**" (f ^ g) = ((D -concatenation) "**" f) ^ ((D -concatenation) "**" g) by Th3;
(D -concatenation) "**" (g ^ f) = ((D -concatenation) "**" g) ^ ((D -concatenation) "**" f) by Th3;
hence ( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) ) by A2, A1, FINSEQ_1:def 7; :: thesis: verum