let p be FinSequence; :: thesis: for x being object
for D being non empty set st x in rng p & p is FinSequence of D holds
p -| x is FinSequence of D
let x be object ; :: thesis: for D being non empty set st x in rng p & p is FinSequence of D holds
p -| x is FinSequence of D
let D be non empty set ; :: thesis: ( x in rng p & p is FinSequence of D implies p -| x is FinSequence of D )
assume x in rng p ; :: thesis: ( not p is FinSequence of D or p -| x is FinSequence of D )
then ex n being Nat st
( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by Def5;
hence ( not p is FinSequence of D or p -| x is FinSequence of D ) by FINSEQ_1:18; :: thesis: verum