let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al holds still_not-bound_in f = union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}

let f be FinSequence of CQC-WFF Al; :: thesis: still_not-bound_in f = union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}

defpred S1[ set ] means ex p being Element of CQC-WFF Al st
( \$1 = still_not-bound_in p & ex i being Nat st
( i in dom f & p = f . i ) );
set X = { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
;
A1: now :: thesis: for b being object st b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
holds
b in still_not-bound_in f
let b be object ; :: thesis: ( b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
implies b in still_not-bound_in f )

assume b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
; :: thesis:
then consider Y being set such that
A2: b in Y and
A3: Y in { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
by TARSKI:def 4;
S1[Y] by A3;
hence b in still_not-bound_in f by ; :: thesis: verum
end;
now :: thesis: for b being object st b in still_not-bound_in f holds
b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
let b be object ; :: thesis: ( b in still_not-bound_in f implies b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
)

assume b in still_not-bound_in f ; :: thesis: b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}

then consider i being Nat, p being Element of CQC-WFF Al such that
A4: ( i in dom f & p = f . i ) and
A5: b in still_not-bound_in p by Def5;
still_not-bound_in p in { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
by A4;
hence b in union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
by ; :: thesis: verum
end;
hence still_not-bound_in f = union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
by ; :: thesis: verum