let p be FinSequence; :: thesis: for A being set
for n being Nat st n = (len p) - (card (p " A)) holds
dom (p - A) = Seg n
let A be set ; :: thesis: for n being Nat st n = (len p) - (card (p " A)) holds
dom (p - A) = Seg n
let n be Nat; :: thesis: ( n = (len p) - (card (p " A)) implies dom (p - A) = Seg n )
assume n = (len p) - (card (p " A)) ; :: thesis: dom (p - A) = Seg n
then len (p - A) = n by Th57;
hence dom (p - A) = Seg n by FINSEQ_1:def 3; :: thesis: verum