let p be FinSequence; :: thesis: for A being set holds len (p - A) <= len p
let A be set ; :: thesis: len (p - A) <= len p
len (p - A) = (len p) - (card (p " A)) by Th57;
hence len (p - A) <= len p by XREAL_1:43; :: thesis: verum