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
(f1 ^ f2) |-- p = (f1 |-- p) ^ f2 by A2, Th8;
then A3: rng ((f1 ^ f2) |-- p) = (rng (f1 |-- p)) \/ (rng f2) by FINSEQ_1:31;
not p in rng ((f1 ^ f2) |-- p) by A1, FINSEQ_4:45;
then not p in rng (f1 |-- p) by A3, XBOOLE_0:def 3;
hence f1 just_once_values p by A2, FINSEQ_4:45; :: thesis: verum