let f be FinSubsequence; :: thesis: for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds
fgh = fg ^ fh

let g, h, fg, fh, fgh be FinSequence; :: thesis: ( rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) implies fgh = fg ^ fh )
assume that
A1: rng g c= dom f and
A2: rng h c= dom f and
A3: fg = f * g and
A4: fh = f * h and
A5: fgh = f * (g ^ h) ; :: thesis: fgh = fg ^ fh
now :: thesis: ( len fgh = (len g) + (len h) & len (fg ^ fh) = (len g) + (len h) & ( for j being Nat st j in dom fgh holds
fgh . j = (fg ^ fh) . j ) )
rng (g ^ h) = (rng g) \/ (rng h) by FINSEQ_1:31;
hence len fgh = len (g ^ h) by
.= (len g) + (len h) by FINSEQ_1:22 ;
:: thesis: ( len (fg ^ fh) = (len g) + (len h) & ( for j being Nat st j in dom fgh holds
fgh . b2 = (fg ^ fh) . b2 ) )

then A6: dom fgh = Seg ((len g) + (len h)) by FINSEQ_1:def 3;
A7: dom fh = dom h by ;
A8: dom fg = dom g by ;
A9: len fg = len g by ;
len fh = len h by ;
hence len (fg ^ fh) = (len g) + (len h) by ; :: thesis: for j being Nat st j in dom fgh holds
fgh . b2 = (fg ^ fh) . b2

let j be Nat; :: thesis: ( j in dom fgh implies fgh . b1 = (fg ^ fh) . b1 )
assume A10: j in dom fgh ; :: thesis: fgh . b1 = (fg ^ fh) . b1
then A11: 1 <= j by ;
A12: j <= (len g) + (len h) by ;
per cases ( j <= len g or len g < j ) ;
suppose j <= len g ; :: thesis: fgh . b1 = (fg ^ fh) . b1
then A13: j in dom g by ;
thus fgh . j = f . ((g ^ h) . j) by
.= f . (g . j) by
.= fg . j by
.= (fg ^ fh) . j by ; :: thesis: verum
end;
suppose len g < j ; :: thesis: fgh . b1 = (fg ^ fh) . b1
then (len g) + 1 <= j by NAT_1:13;
then A14: 1 <= j - (len g) by XREAL_1:19;
then j -' (len g) = j - (len g) by XREAL_0:def 2;
then reconsider j9 = j - (len g) as Element of NAT ;
A15: j = (len g) + j9 ;
then j9 <= len h by ;
then A16: j9 in dom h by ;
thus fgh . j = f . ((g ^ h) . j) by
.= f . (h . j9) by
.= fh . j9 by
.= (fg ^ fh) . j by ; :: thesis: verum
end;
end;
end;
hence fgh = fg ^ fh by FINSEQ_2:9; :: thesis: verum