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 ;
then A3: (f1 ^ f2) . ((len f1) + (p .. f2)) = p by ;
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) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2)) )
assume that
A5: 1 <= i and
A6: i < (len f1) + (p .. f2) ; :: thesis: not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2))
per cases ( i <= len f1 or i > len f1 ) ;
suppose i <= len f1 ; :: thesis: not (f1 ^ f2) . b1 = (f1 ^ f2) . ((len f1) + (p .. f2))
then A7: i in dom f1 by ;
assume (f1 ^ f2) . i = (f1 ^ f2) . ((len f1) + (p .. f2)) ; :: thesis: contradiction
then f1 . i = p by ;
then p in rng f1 by ;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum
end;
suppose A8: i > len f1 ; :: thesis: (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 ;
then A9: 1 <= j by NAT_1:14;
A10: i = j + (len f1) ;
then A11: j < p .. f2 by ;
A12: (f1 ^ f2) . ((len f1) + (p .. f2)) = f2 . (p .. f2) by ;
A13: p .. f2 <= len f2 by ;
j <= p .. f2 by ;
then j <= len f2 by ;
then A14: j in dom f2 by ;
then (f1 ^ f2) . i = f2 . j by ;
hence (f1 ^ f2) . i <> (f1 ^ f2) . ((len f1) + (p .. f2)) by ; :: thesis: verum
end;
end;
end;
(len f1) + (p .. f2) in dom (f1 ^ f2) by ;
hence p .. (f1 ^ f2) = (len f1) + (p .. f2) by A3, A4, Th2; :: thesis: verum