let f1, f2 be FinSequence; :: thesis: for p being set st p in (rng f2) \ (rng f1) holds
p .. (f1 ^ f2) = (len f1) + (p .. f2)
let p be set ; :: thesis: ( p in (rng f2) \ (rng f1) implies p .. (f1 ^ f2) = (len f1) + (p .. f2) )
assume A1: p in (rng f2) \ (rng f1) ; :: thesis: 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 :: thesis: 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; :: thesis: ( 1 <= i & i < (len f1) + (p .. f2) implies not (f1 ^ f2) . b₁ = (f1 ^ f2) . ((len f1) + (p .. f2)) )
assume that
A5: 1 <= i and
A6: i < (len f1) + (p .. f2) ; :: thesis: not (f1 ^ f2) . b₁ = (f1 ^ f2) . ((len f1) + (p .. f2))

per cases ( i <= len f1 or i > len f1 ) ;

suppose i <= len f1 ; :: thesis: not (f1 ^ f2) . b₁ = (f1 ^ f2) . ((len f1) + (p .. f2))

then A7: i in dom f1 by A5, FINSEQ_3:25;
assume (f1 ^ f2) . i = (f1 ^ f2) . ((len f1) + (p .. f2)) ; :: thesis: contradiction
then f1 . i = p by A3, A7, FINSEQ_1:def 7;
then p in rng f1 by A7, FUNCT_1:def 3;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A8: i > len f1 ; :: thesis: (f1 ^ f2) . b₁ <> (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; :: thesis: 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; :: thesis: verum