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

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*>

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;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

now :: thesis: for b being object st b in still_not-bound_in <*p*> holds

b in still_not-bound_in p

hence
still_not-bound_in <*p*> = still_not-bound_in p
by A1, TARSKI:2; :: thesis: verumb 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;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