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 A1, A2, A5, FINSEQ_2:29, XBOOLE_1:8
.= (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 . b₂ = (fg ^ fh) . b₂ ) )
then A6: dom fgh = Seg ((len g) + (len h)) by FINSEQ_1:def 3;
A7: dom fh = dom h by A2, A4, RELAT_1:27;
A8: dom fg = dom g by A1, A3, RELAT_1:27;
A9: len fg = len g by A1, A3, FINSEQ_2:29;
len fh = len h by A2, A4, FINSEQ_2:29;
hence len (fg ^ fh) = (len g) + (len h) by A9, FINSEQ_1:22; :: thesis: for j being Nat st j in dom fgh holds
fgh . b₂ = (fg ^ fh) . b₂
let j be Nat; :: thesis: ( j in dom fgh implies fgh . b₁ = (fg ^ fh) . b₁ )
assume A10: j in dom fgh ; :: thesis: fgh . b₁ = (fg ^ fh) . b₁
then A11: 1 <= j by A6, FINSEQ_1:1;
A12: j <= (len g) + (len h) by A6, A10, FINSEQ_1:1;

per cases ( j <= len g or len g < j ) ;

suppose j <= len g ; :: thesis: fgh . b₁ = (fg ^ fh) . b₁

then A13: j in dom g by A11, FINSEQ_3:25;
thus fgh . j = f . ((g ^ h) . j) by A5, A10, FUNCT_1:12
.= f . (g . j) by A13, FINSEQ_1:def 7
.= fg . j by A3, A13, FUNCT_1:13
.= (fg ^ fh) . j by A8, A13, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose len g < j ; :: thesis: fgh . b₁ = (fg ^ fh) . b₁

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 A12, XREAL_1:6;
then A16: j9 in dom h by A14, FINSEQ_3:25;
thus fgh . j = f . ((g ^ h) . j) by A5, A10, FUNCT_1:12
.= f . (h . j9) by A15, A16, FINSEQ_1:def 7
.= fh . j9 by A4, A16, FUNCT_1:13
.= (fg ^ fh) . j by A9, A7, A15, A16, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence fgh = fg ^ fh by FINSEQ_2:9; :: thesis: verum