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 ;
A4: dom (f * B) = dom B by ;
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 ;
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 ;
A8: dom (f * A) = dom A by ;
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
let k be Nat; :: thesis: ( 1 <= k & k <= len fAB implies (fA ^ fB) . b1 = fAB . b1 )
assume ( 1 <= k & k <= len fAB ) ; :: thesis: (fA ^ fB) . b1 = fAB . b1
then A11: k in dom fAB by FINSEQ_3:25;
per cases ( k in dom fA or not k in dom fA ) ;
suppose A12: k in dom fA ; :: thesis: (fA ^ fB) . b1 = fAB . b1
hence (fA ^ fB) . k = fA . k by FINSEQ_1:def 7
.= f . (A . k) by
.= f . ((A ^ B) . k) by
.= fAB . k by ;
:: thesis: verum
end;
suppose not k in dom fA ; :: thesis: fAB . b1 = (fA ^ fB) . b1
then consider n being Nat such that
A13: n in dom B and
A14: k = (len A) + n by ;
thus fAB . k = f . ((A ^ B) . k) by
.= f . (B . n) by
.= fB . n by
.= (fA ^ fB) . k by ; :: thesis: verum
end;
end;
end;
len fAB = len (A ^ B) by
.= (len fA) + (len fB) by
.= len (fA ^ fB) by FINSEQ_1:22 ;
hence ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) by ; :: thesis: verum