let p be FinSequence; :: thesis: for A being set holds (p ^ {}) - A = (p - A) ^ ({} - A)
let A be set ; :: thesis: (p ^ {}) - A = (p - A) ^ ({} - A)
thus (p ^ {}) - A = p - A by FINSEQ_1:34
.= (p - A) ^ ({} - A) by FINSEQ_1:34 ; :: thesis: verum