let p be set ; :: thesis: for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) |-- p = g
let D be non empty set ; :: thesis: for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) |-- p = g
let f be non empty FinSequence of D; :: thesis: for g being FinSequence of D st p .. f = len f holds
(f ^ g) |-- p = g
let g be FinSequence of D; :: thesis: ( p .. f = len f implies (f ^ g) |-- p = g )
assume A1: p .. f = len f ; :: thesis: (f ^ g) |-- p = g
A2: p in rng f by A1, Th4;
then A3: p .. (f ^ g) = len f by A1, FINSEQ_6:6;
rng f c= rng (f ^ g) by FINSEQ_1:29;
hence (f ^ g) |-- p = (f ^ g) /^ (p .. (f ^ g)) by A2, FINSEQ_5:35
.= g by A3 ;
:: thesis: verum