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

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 ) )

hence
fgh = fg ^ fh
by FINSEQ_2:9; :: thesis: verumfgh . 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_{2} = (fg ^ fh) . b_{2} ) )

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_{2} = (fg ^ fh) . b_{2}

let j be Nat; :: thesis: ( j in dom fgh implies fgh . b_{1} = (fg ^ fh) . b_{1} )

assume A10: j in dom fgh ; :: thesis: fgh . b_{1} = (fg ^ fh) . b_{1}

then A11: 1 <= j by A6, FINSEQ_1:1;

A12: j <= (len g) + (len h) by A6, A10, FINSEQ_1:1;

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

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

let j be Nat; :: thesis: ( j in dom fgh implies fgh . b

assume A10: j in dom fgh ; :: thesis: fgh . 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 )
;

end;

suppose
j <= len g
; :: thesis: fgh . b_{1} = (fg ^ fh) . b_{1}

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

suppose
len g < j
; :: thesis: fgh . b_{1} = (fg ^ fh) . b_{1}

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