let D be non empty set ; :: thesis: for p being Element of D
for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -: p = f1 ^ (f2 -: p)
let p be Element of D; :: thesis: for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -: p = f1 ^ (f2 -: p)
let f1, f2 be FinSequence of D; :: thesis: ( p in (rng f2) \ (rng f1) implies (f1 ^ f2) -: p = f1 ^ (f2 -: p) )
assume A1: p in (rng f2) \ (rng f1) ; :: thesis: (f1 ^ f2) -: p = f1 ^ (f2 -: p)
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 = ((f1 ^ f2) -| p) ^ <*p*> by Th40
.= (f1 ^ (f2 -| p)) ^ <*p*> by A1, Th15
.= f1 ^ ((f2 -| p) ^ <*p*>) by FINSEQ_1:32
.= f1 ^ (f2 -: p) by A1, Th40 ;
:: thesis: verum