let f1, f2 be FinSequence; for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
let i be Nat; (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
A1:
dom (f1 ^ (f2 | (Seg i))) c= Seg ((len f1) + i)
A9:
(dom (f1 ^ f2)) /\ (Seg ((len f1) + i)) c= dom (f1 ^ (f2 | (Seg i)))
A17:
dom ((f1 ^ f2) | (Seg ((len f1) + i))) = (dom (f1 ^ f2)) /\ (Seg ((len f1) + i))
by RELAT_1:61;
A18:
now for k being Nat st k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) holds
((f1 ^ f2) | (Seg ((len f1) + i))) . k = (f1 ^ (f2 | (Seg i))) . klet k be
Nat;
( k in dom ((f1 ^ f2) | (Seg ((len f1) + i))) implies ((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1 )assume A19:
k in dom ((f1 ^ f2) | (Seg ((len f1) + i)))
;
((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1then A20:
1
<= k
by FINSEQ_3:25;
per cases
( k <= len f1 or k > len f1 )
;
suppose A22:
k > len f1
;
((f1 ^ f2) | (Seg ((len f1) + i))) . b1 = (f1 ^ (f2 | (Seg i))) . b1then reconsider j =
k - (len f1) as
Element of
NAT by INT_1:5;
j > 0
by A22, XREAL_1:50;
then A23:
1
<= j
by NAT_1:14;
A24:
k = (len f1) + j
;
A25:
not
k in dom f1
by A22, FINSEQ_3:25;
k in dom (f1 ^ f2)
by A17, A19, XBOOLE_0:def 4;
then A26:
ex
n being
Nat st
(
n in dom f2 &
k = (len f1) + n )
by A25, FINSEQ_1:25;
k in Seg ((len f1) + i)
by A17, A19, XBOOLE_0:def 4;
then
k <= (len f1) + i
by FINSEQ_1:1;
then
j <= i
by A24, XREAL_1:6;
then A27:
j in Seg i
by A23;
dom (f2 | (Seg i)) = (dom f2) /\ (Seg i)
by RELAT_1:61;
then A28:
j in dom (f2 | (Seg i))
by A27, A26, XBOOLE_0:def 4;
thus ((f1 ^ f2) | (Seg ((len f1) + i))) . k =
(f1 ^ f2) . k
by A19, FUNCT_1:47
.=
f2 . j
by A26, FINSEQ_1:def 7
.=
(f2 | (Seg i)) . j
by A28, FUNCT_1:47
.=
(f1 ^ (f2 | (Seg i))) . k
by A24, A28, FINSEQ_1:def 7
;
verum end; end; end;
f1 ^ (f2 | (Seg i)) c= f1 ^ f2
by Th13, RELAT_1:59;
then
dom (f1 ^ (f2 | (Seg i))) c= dom (f1 ^ f2)
by RELAT_1:11;
then
dom (f1 ^ (f2 | (Seg i))) c= (dom (f1 ^ f2)) /\ (Seg ((len f1) + i))
by A1, XBOOLE_1:19;
then
dom ((f1 ^ f2) | (Seg ((len f1) + i))) = dom (f1 ^ (f2 | (Seg i)))
by A17, A9;
hence
(f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
by A18, FINSEQ_1:13; verum