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;

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) . b₁ = fAB . b₁ )
assume ( 1 <= k & k <= len fAB ) ; :: thesis: (fA ^ fB) . b₁ = fAB . b₁
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) . b₁ = fAB . b₁

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;

suppose not k in dom fA ; :: thesis: fAB . b₁ = (fA ^ fB) . b₁

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;

end;

end;

len fAB = len (A ^ B) by A7, 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