let f1, f2 be FinSequence; :: thesis: for p being set st f1 ^ f2 just_once_values p holds
p in (rng f1) \+\ (rng f2)
let p be set ; :: thesis: ( f1 ^ f2 just_once_values p implies p in (rng f1) \+\ (rng f2) )
A1: rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
assume A2: f1 ^ f2 just_once_values p ; :: thesis: p in (rng f1) \+\ (rng f2)

A3: now :: thesis: not p in (rng f1) /\ (rng f2)

assume A4: p in (rng f1) /\ (rng f2) ; :: thesis: contradiction
then p in rng f1 by XBOOLE_0:def 4;
then (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by Th8;
then A5: not p in rng ((f1 |-- p) ^ f2) by A2, FINSEQ_4:45;
rng ((f1 |-- p) ^ f2) = (rng (f1 |-- p)) \/ (rng f2) by FINSEQ_1:31;
then not p in rng f2 by A5, XBOOLE_0:def 3;
hence contradiction by A4, XBOOLE_0:def 4; :: thesis: verum

end;

p in rng (f1 ^ f2) by A2, FINSEQ_4:5;
then p in ((rng f1) \/ (rng f2)) \ ((rng f1) /\ (rng f2)) by A1, A3, XBOOLE_0:def 5;
hence p in (rng f1) \+\ (rng f2) by XBOOLE_1:101; :: thesis: verum