let f1, f2 be FinSequence; for p being set st p in (rng f2) \ (rng f1) holds
p .. (f1 ^ f2) = (len f1) + (p .. f2)
let p be set ; ( p in (rng f2) \ (rng f1) implies p .. (f1 ^ f2) = (len f1) + (p .. f2) )
assume A1:
p in (rng f2) \ (rng f1)
; p .. (f1 ^ f2) = (len f1) + (p .. f2)
then A2:
p .. f2 in dom f2
by FINSEQ_4:20;
f2 . (p .. f2) = p
by A1, FINSEQ_4:19;
then A3:
(f1 ^ f2) . ((len f1) + (p .. f2)) = p
by A2, FINSEQ_1:def 7;
A4:
now for i being Nat st 1 <= i & i < (len f1) + (p .. f2) holds
not (f1 ^ f2) . i = (f1 ^ f2) . ((len f1) + (p .. f2))let i be
Nat;
( 1 <= i & i < (len f1) + (p .. f2) implies not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2)) )assume that A5:
1
<= i
and A6:
i < (len f1) + (p .. f2)
;
not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2))per cases
( i <= len f1 or i > len f1 )
;
suppose A8:
i > len f1
;
(f1 ^ f2) . b1 <> (f1 ^ f2) . ((len f1) + (p .. f2))then reconsider j =
i - (len f1) as
Element of
NAT by INT_1:5;
j > 0
by A8, XREAL_1:50;
then A9:
1
<= j
by NAT_1:14;
A10:
i = j + (len f1)
;
then A11:
j < p .. f2
by A6, XREAL_1:6;
A12:
(f1 ^ f2) . ((len f1) + (p .. f2)) = f2 . (p .. f2)
by A2, FINSEQ_1:def 7;
A13:
p .. f2 <= len f2
by A1, FINSEQ_4:21;
j <= p .. f2
by A6, A10, XREAL_1:6;
then
j <= len f2
by A13, XXREAL_0:2;
then A14:
j in dom f2
by A9, FINSEQ_3:25;
then
(f1 ^ f2) . i = f2 . j
by A10, FINSEQ_1:def 7;
hence
(f1 ^ f2) . i <> (f1 ^ f2) . ((len f1) + (p .. f2))
by A1, A11, A14, A12, FINSEQ_4:19, FINSEQ_4:24;
verum end; end; end;
(len f1) + (p .. f2) in dom (f1 ^ f2)
by A2, FINSEQ_1:28;
hence
p .. (f1 ^ f2) = (len f1) + (p .. f2)
by A3, A4, Th2; verum