let f2, f1 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: f2 . (p .. f2) = p by FINSEQ_4:29;
A3: p .. f2 in dom f2 by A1, FINSEQ_4:30;
then A4: (f1 ^ f2) . ((len f1) + (p .. f2)) = p by A2, FINSEQ_1:def 7;
A5: (len f1) + (p .. f2) in dom (f1 ^ f2) by A3, FINSEQ_1:41;

now

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
A6: 1 <= i and
A7: 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 A8: i in dom f1 by A6, FINSEQ_3:27;
assume (f1 ^ f2) . i = (f1 ^ f2) . ((len f1) + (p .. f2)) ; :: thesis: contradiction
then f1 . i = p by A4, A8, FINSEQ_1:def 7;
then p in rng f1 by A8, FUNCT_1:def 5;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A9: 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:18;
A10: i = j + (len f1) ;
j > 0 by A9, XREAL_1:52;
then A11: 1 <= j by NAT_1:14;
A12: j < p .. f2 by A7, A10, XREAL_1:8;
( j <= p .. f2 & p .. f2 <= len f2 ) by A1, A7, A10, FINSEQ_4:31, XREAL_1:8;
then j <= len f2 by XXREAL_0:2;
then A13: j in dom f2 by A11, FINSEQ_3:27;
A14: (f1 ^ f2) . ((len f1) + (p .. f2)) = f2 . (p .. f2) by A3, FINSEQ_1:def 7;
(f1 ^ f2) . i = f2 . j by A10, A13, FINSEQ_1:def 7;
hence (f1 ^ f2) . i <> (f1 ^ f2) . ((len f1) + (p .. f2)) by A1, A12, A13, A14, FINSEQ_4:29, FINSEQ_4:34; :: thesis: verum

end;

end;

end;

hence p .. (f1 ^ f2) = (len f1) + (p .. f2) by A4, A5, Th4; :: thesis: verum