let i be Nat; for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f
let D be non empty set ; for p being Element of D
for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f
let p be Element of D; for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f
let f be FinSequence of D; ( p in rng (f | i) implies p .. (f | i) = p .. f )
A1:
dom (f | i) c= dom f
by Th18;
assume A2:
p in rng (f | i)
; p .. (f | i) = p .. f
then A3:
p .. (f | i) in dom (f | i)
by FINSEQ_4:20;
then f /. (p .. (f | i)) =
(f | i) /. (p .. (f | i))
by FINSEQ_4:70
.=
p
by A2, Th38
;
then A4:
p .. f <= p .. (f | i)
by A3, A1, Th39;
p .. (f | i) <= len (f | i)
by A2, FINSEQ_4:21;
then A5:
p .. f <= len (f | i)
by A4, XXREAL_0:2;
A6:
rng (f | i) c= rng f
by Th19;
then
1 <= p .. f
by A2, FINSEQ_4:21;
then A7:
p .. f in dom (f | i)
by A5, FINSEQ_3:25;
then (f | i) /. (p .. f) =
f /. (p .. f)
by FINSEQ_4:70
.=
p
by A2, A6, Th38
;
then
p .. (f | i) <= p .. f
by A7, Th39;
hence
p .. (f | i) = p .. f
by A4, XXREAL_0:1; verum