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:47
.= (p - A) ^ ({} - A) by FINSEQ_1:47 ; :: thesis: verum