let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds still_not-bound_in <*p*> = still_not-bound_in p
let p be Element of CQC-WFF Al; :: thesis: still_not-bound_in <*p*> = still_not-bound_in p
A1: now :: thesis: for b being object st b in still_not-bound_in p holds
b in still_not-bound_in <*p*>
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then A2: 1 in dom <*p*> by FINSEQ_1:38;
A3: p = <*p*> . 1 by FINSEQ_1:40;
let b be object ; :: thesis: ( b in still_not-bound_in p implies b in still_not-bound_in <*p*> )
assume b in still_not-bound_in p ; :: thesis: b in still_not-bound_in <*p*>
hence b in still_not-bound_in <*p*> by A2, A3, Def5; :: thesis: verum
end;
now :: thesis: for b being object st b in still_not-bound_in <*p*> holds
b in still_not-bound_in p
let b be object ; :: thesis: ( b in still_not-bound_in <*p*> implies b in still_not-bound_in p )
assume b in still_not-bound_in <*p*> ; :: thesis: b in still_not-bound_in p
then consider i being Nat, q being Element of CQC-WFF Al such that
A4: i in dom <*p*> and
A5: ( q = <*p*> . i & b in still_not-bound_in q ) by Def5;
i in Seg 1 by A4, FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def 1;
hence b in still_not-bound_in p by A5, FINSEQ_1:40; :: thesis: verum
end;
hence still_not-bound_in <*p*> = still_not-bound_in p by A1, TARSKI:2; :: thesis: verum