let A, B be FinSequence; 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; ( (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
; 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
; ex fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
take
fB
; ( 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 for k being Nat st 1 <= k & k <= len fAB holds
(fA ^ fB) . k = fAB . klet k be
Nat;
( 1 <= k & k <= len fAB implies (fA ^ fB) . b1 = fAB . b1 )assume
( 1
<= k &
k <= len fAB )
;
(fA ^ fB) . b1 = fAB . b1then A11:
k in dom fAB
by FINSEQ_3:25;
per cases
( k in dom fA or not k in dom fA )
;
suppose
not
k in dom fA
;
fAB . b1 = (fA ^ fB) . b1then 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
;
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; verum