let p be FinSequence; :: thesis: for x being object
for k being Nat st x in rng p & k in dom (p -| x) holds
p . k = (p -| x) . k
let x be object ; :: thesis: for k being Nat st x in rng p & k in dom (p -| x) holds
p . k = (p -| x) . k
let k be Nat; :: thesis: ( x in rng p & k in dom (p -| x) implies p . k = (p -| x) . k )
assume that
A1: x in rng p and
A2: k in dom (p -| x) ; :: thesis: p . k = (p -| x) . k
ex n being Nat st
( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by A1, Def5;
hence p . k = (p -| x) . k by A2, FUNCT_1:47; :: thesis: verum