let f1, f2 be FinSequence; :: thesis: for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds
f1 just_once_values p
let p be set ; :: thesis: ( f1 ^ f2 just_once_values p & p in rng f1 implies f1 just_once_values p )
assume that
A1: f1 ^ f2 just_once_values p and
A2: p in rng f1 ; :: thesis: f1 just_once_values p
A3: not p in rng ((f1 ^ f2) |-- p) by A1, FINSEQ_4:60;
(f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A2, Th10;
then rng ((f1 ^ f2) |-- p) = (rng (f1 |-- p)) \/ (rng f2) by FINSEQ_1:44;
then not p in rng (f1 |-- p) by A3, XBOOLE_0:def 3;
hence f1 just_once_values p by A2, FINSEQ_4:60; :: thesis: verum