let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)
let Al2 be Al -expanding QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)
defpred S₁[ Element of CQC-WFF Al] means still_not-bound_in $1 = still_not-bound_in (Al2 -Cast $1);
A1: S₁[ VERUM Al]

proof

thus still_not-bound_in (VERUM Al) = {} by QC_LANG3:3
.= still_not-bound_in (VERUM Al2) by QC_LANG3:3
.= still_not-bound_in (Al2 -Cast (VERUM Al)) ; :: thesis: verum

end;

A2: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S₁[P ! l]

proof

let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S₁[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S₁[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S₁[P ! l]
A3: still_not-bound_in l = still_not-bound_in (Al2 -Cast l)

proof

for x being object st x in still_not-bound_in l holds
x in still_not-bound_in (Al2 -Cast l)

proof

let x be object ; :: thesis: ( x in still_not-bound_in l implies x in still_not-bound_in (Al2 -Cast l) )
assume A4: x in still_not-bound_in l ; :: thesis: x in still_not-bound_in (Al2 -Cast l)
consider n being Nat such that
A5: ( x = l . n & 1 <= n & n <= len l & l . n in bound_QC-variables Al ) by A4;
set y = l . n;
reconsider y = l . n as bound_QC-variable of Al by A5;
y = Al2 -Cast y ;
hence x in still_not-bound_in (Al2 -Cast l) by A5; :: thesis: verum

end;

hence still_not-bound_in l c= still_not-bound_in (Al2 -Cast l) ; :: according to XBOOLE_0:def 10 :: thesis: still_not-bound_in (Al2 -Cast l) c= still_not-bound_in l
for x being object st x in still_not-bound_in (Al2 -Cast l) holds
x in still_not-bound_in l

proof

let x be object ; :: thesis: ( x in still_not-bound_in (Al2 -Cast l) implies x in still_not-bound_in l )
assume A6: x in still_not-bound_in (Al2 -Cast l) ; :: thesis: x in still_not-bound_in l
consider n being Nat such that
A7: ( x = (Al2 -Cast l) . n & 1 <= n & n <= len (Al2 -Cast l) & (Al2 -Cast l) . n in bound_QC-variables Al2 ) by A6;
set y = (Al2 -Cast l) . n;
( rng l c= bound_QC-variables Al & dom l = Seg (len l) ) by FINSEQ_1:def 3;
then ( (Al2 -Cast l) . n = l . n & n in dom l & l is FinSequence of bound_QC-variables Al ) by A7, FINSEQ_1:1, FINSEQ_1:def 4;
then (Al2 -Cast l) . n in bound_QC-variables Al by FINSEQ_2:11;
hence x in still_not-bound_in l by A7; :: thesis: verum

end;

hence still_not-bound_in (Al2 -Cast l) c= still_not-bound_in l ; :: thesis: verum

end;

thus still_not-bound_in (P ! l) = still_not-bound_in l by QC_LANG3:5
.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by A3, QC_LANG3:5
.= still_not-bound_in (Al2 -Cast (P ! l)) by Th8 ; :: thesis: verum

end;

A8: for p being Element of CQC-WFF Al st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of CQC-WFF Al; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A9: S₁[p] ; :: thesis: S₁[ 'not' p]
thus still_not-bound_in ('not' p) = still_not-bound_in p by QC_LANG3:7
.= still_not-bound_in ('not' (Al2 -Cast p)) by A9, QC_LANG3:7
.= still_not-bound_in (Al2 -Cast ('not' p)) ; :: thesis: verum

end;

A10: for p, q being Element of CQC-WFF Al st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of CQC-WFF Al; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A11: ( S₁[p] & S₁[q] ) ; :: thesis: S₁[p '&' q]
set p2 = Al2 -Cast p;
set q2 = Al2 -Cast q;
reconsider p2 = Al2 -Cast p, q2 = Al2 -Cast q as Element of CQC-WFF Al2 ;
( p '&' q is conjunctive & p2 '&' q2 is conjunctive ) ;
then A12: ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) & p2 = the_left_argument_of (p2 '&' q2) & q2 = the_right_argument_of (p2 '&' q2) ) by QC_LANG1:def 25, QC_LANG1:def 26;
hence still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG1:def 20, QC_LANG3:9
.= still_not-bound_in (Al2 -Cast (p '&' q)) by A11, A12, QC_LANG1:def 20, QC_LANG3:9 ;
:: thesis: verum

end;

for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st S₁[p] holds
S₁[ All (x,p)]

proof

let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al st S₁[p] holds
S₁[ All (x,p)]
let p be Element of CQC-WFF Al; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume A13: S₁[p] ; :: thesis: S₁[ All (x,p)]
set x2 = Al2 -Cast x;
set p2 = Al2 -Cast p;
reconsider p2 = Al2 -Cast p as Element of CQC-WFF Al2 ;
reconsider x2 = Al2 -Cast x as bound_QC-variable of Al2 ;
( All (x,p) is universal & All (x2,p2) is universal ) ;
then A14: ( p = the_scope_of (All (x,p)) & x = bound_in (All (x,p)) & p2 = the_scope_of (All (x2,p2)) & x2 = bound_in (All (x2,p2)) ) by QC_LANG1:def 27, QC_LANG1:def 28;
then still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:11, QC_LANG1:def 21
.= still_not-bound_in (Al2 -Cast (All (x,p))) by A13, A14, QC_LANG1:def 21, QC_LANG3:11 ;
hence S₁[ All (x,p)] ; :: thesis: verum

end;

then A15: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! l] & ( S₁[p] implies S₁[ 'not' p] ) & ( S₁[p] & S₁[q] implies S₁[p '&' q] ) & ( S₁[p] implies S₁[ All (x,p)] ) ) by A1, A2, A8, A10;
for p being Element of CQC-WFF Al holds S₁[p] from CQC_LANG:sch 1(A15);
hence for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p) ; :: thesis: verum