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 )
A2: rng A c= (rng A) \/ (rng B) by XBOOLE_1:7;
then reconsider fA = f * A as FinSequence by A1, FINSEQ_1:20, XBOOLE_1:1;
A3: dom (f * A) = dom A by A1, A2, RELAT_1:46, XBOOLE_1:1;
then A4: len fA = len A by FINSEQ_3:31;
A5: rng B c= (rng A) \/ (rng B) by XBOOLE_1:7;
then reconsider fB = f * B as FinSequence by A1, FINSEQ_1:20, XBOOLE_1:1;
A6: dom (f * B) = dom B by A1, A5, RELAT_1:46, XBOOLE_1:1;
then A7: len fB = len B by FINSEQ_3:31;
A8: rng (A ^ B) c= dom f by A1, FINSEQ_1:44;
then reconsider fAB = f * (A ^ B) as FinSequence by FINSEQ_1:20;
A9: dom (f * (A ^ B)) = dom (A ^ B) by A8, RELAT_1:46;
then A10: len fAB = len (A ^ B) by FINSEQ_3:31
.= (len fA) + (len fB) by A4, A7, FINSEQ_1:35
.= len (fA ^ fB) by FINSEQ_1:35 ;
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 )

now

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

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:22
.= f . ((A ^ B) . k) by A3, A12, FINSEQ_1:def 7
.= fAB . k by A11, FUNCT_1:22 ;
:: 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 & k = (len A) + n ) by A3, A9, A11, FINSEQ_1:38;
thus fAB . k = f . ((A ^ B) . k) by A11, FUNCT_1:22
.= f . (B . n) by A13, FINSEQ_1:def 7
.= fB . n by A6, A13, FUNCT_1:22
.= (fA ^ fB) . k by A4, A6, A13, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

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