defpred S₁[ FinSequence] means for p being FinSequence
for A being set holds (p ^ $1) - A = (p - A) ^ ($1 - A);
A1: for q being FinSequence
for x being object st S₁[q] holds
S₁[q ^ <*x*>] by Lm10;
A2: S₁[ {} ] by Lm8;
for q being FinSequence holds S₁[q] from FINSEQ_1:sch 3(A2, A1);
hence for q, p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A) ; :: thesis: verum