let D be non empty set ; :: thesis: for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) :- p = (f1 :- p) ^ f2
let p be Element of D; :: thesis: for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) :- p = (f1 :- p) ^ f2
let f1, f2 be FinSequence of D; :: thesis: ( p in rng f1 implies (f1 ^ f2) :- p = (f1 :- p) ^ f2 )
assume A1: p in rng f1 ; :: thesis: (f1 ^ f2) :- p = (f1 :- p) ^ f2
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then p in rng (f1 ^ f2) by A1, XBOOLE_0:def 3;
hence (f1 ^ f2) :- p = <*p*> ^ ((f1 ^ f2) |-- p) by Th41
.= <*p*> ^ ((f1 |-- p) ^ f2) by A1, Th8
.= (<*p*> ^ (f1 |-- p)) ^ f2 by FINSEQ_1:32
.= (f1 :- p) ^ f2 by A1, Th41 ;
:: thesis: verum