let A, B be FinSequence; :: thesis: for f being Function st (rng A) \/ (rng B) c= dom f holds

ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

let f be Function; :: thesis: ( (rng A) \/ (rng B) c= dom f implies ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) )

assume A1: (rng A) \/ (rng B) c= dom f ; :: thesis: ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

then A2: rng (A ^ B) c= dom f by FINSEQ_1:31;

then reconsider fAB = f * (A ^ B) as FinSequence by FINSEQ_1:16;

A3: rng B c= (rng A) \/ (rng B) by XBOOLE_1:7;

then reconsider fB = f * B as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;

A4: dom (f * B) = dom B by A1, A3, RELAT_1:27, XBOOLE_1:1;

then A5: len fB = len B by FINSEQ_3:29;

A6: rng A c= (rng A) \/ (rng B) by XBOOLE_1:7;

then reconsider fA = f * A as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;

take fA ; :: thesis: ex fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

take fB ; :: thesis: ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

A7: dom (f * (A ^ B)) = dom (A ^ B) by A2, RELAT_1:27;

A8: dom (f * A) = dom A by A1, A6, RELAT_1:27, XBOOLE_1:1;

then A9: len fA = len A by FINSEQ_3:29;

.= (len fA) + (len fB) by A9, A5, FINSEQ_1:22

.= len (fA ^ fB) by FINSEQ_1:22 ;

hence ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) by A10, FINSEQ_1:14; :: thesis: verum

ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

let f be Function; :: thesis: ( (rng A) \/ (rng B) c= dom f implies ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) )

assume A1: (rng A) \/ (rng B) c= dom f ; :: thesis: ex fA, fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

then A2: rng (A ^ B) c= dom f by FINSEQ_1:31;

then reconsider fAB = f * (A ^ B) as FinSequence by FINSEQ_1:16;

A3: rng B c= (rng A) \/ (rng B) by XBOOLE_1:7;

then reconsider fB = f * B as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;

A4: dom (f * B) = dom B by A1, A3, RELAT_1:27, XBOOLE_1:1;

then A5: len fB = len B by FINSEQ_3:29;

A6: rng A c= (rng A) \/ (rng B) by XBOOLE_1:7;

then reconsider fA = f * A as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;

take fA ; :: thesis: ex fB being FinSequence st

( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

take fB ; :: thesis: ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )

A7: dom (f * (A ^ B)) = dom (A ^ B) by A2, RELAT_1:27;

A8: dom (f * A) = dom A by A1, A6, RELAT_1:27, XBOOLE_1:1;

then A9: len fA = len A by FINSEQ_3:29;

A10: now :: thesis: for k being Nat st 1 <= k & k <= len fAB holds

(fA ^ fB) . k = fAB . k

len fAB =
len (A ^ B)
by A7, FINSEQ_3:29
(fA ^ fB) . k = fAB . k

let k be Nat; :: thesis: ( 1 <= k & k <= len fAB implies (fA ^ fB) . b_{1} = fAB . b_{1} )

assume ( 1 <= k & k <= len fAB ) ; :: thesis: (fA ^ fB) . b_{1} = fAB . b_{1}

then A11: k in dom fAB by FINSEQ_3:25;

end;assume ( 1 <= k & k <= len fAB ) ; :: thesis: (fA ^ fB) . b

then A11: k in dom fAB by FINSEQ_3:25;

per cases
( k in dom fA or not k in dom fA )
;

end;

suppose A12:
k in dom fA
; :: thesis: (fA ^ fB) . b_{1} = fAB . b_{1}

hence (fA ^ fB) . k =
fA . k
by FINSEQ_1:def 7

.= f . (A . k) by A12, FUNCT_1:12

.= f . ((A ^ B) . k) by A8, A12, FINSEQ_1:def 7

.= fAB . k by A11, FUNCT_1:12 ;

:: thesis: verum

end;.= f . (A . k) by A12, FUNCT_1:12

.= f . ((A ^ B) . k) by A8, A12, FINSEQ_1:def 7

.= fAB . k by A11, FUNCT_1:12 ;

:: thesis: verum

suppose
not k in dom fA
; :: thesis: fAB . b_{1} = (fA ^ fB) . b_{1}

then consider n being Nat such that

A13: n in dom B and

A14: k = (len A) + n by A8, A7, A11, FINSEQ_1:25;

thus fAB . k = f . ((A ^ B) . k) by A11, FUNCT_1:12

.= f . (B . n) by A13, A14, FINSEQ_1:def 7

.= fB . n by A4, A13, FUNCT_1:12

.= (fA ^ fB) . k by A9, A4, A13, A14, FINSEQ_1:def 7 ; :: thesis: verum

end;A13: n in dom B and

A14: k = (len A) + n by A8, A7, A11, FINSEQ_1:25;

thus fAB . k = f . ((A ^ B) . k) by A11, FUNCT_1:12

.= f . (B . n) by A13, A14, FINSEQ_1:def 7

.= fB . n by A4, A13, FUNCT_1:12

.= (fA ^ fB) . k by A9, A4, A13, A14, FINSEQ_1:def 7 ; :: thesis: verum

.= (len fA) + (len fB) by A9, A5, FINSEQ_1:22

.= len (fA ^ fB) by FINSEQ_1:22 ;

hence ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) by A10, FINSEQ_1:14; :: thesis: verum