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 S1[ Element of CQC-WFF Al] means still_not-bound_in \$1 = still_not-bound_in (Al2 -Cast \$1);
A1: S1[ VERUM Al]
proof 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 S1[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 S1[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S1[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S1[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:
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:
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 ;
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
.= still_not-bound_in (Al2 -Cast (P ! l)) by Th8 ; :: thesis: verum
end;
A8: for p being Element of CQC-WFF Al st S1[p] holds
S1[ 'not' p]
proof
let p be Element of CQC-WFF Al; :: thesis: ( S1[p] implies S1[ 'not' p] )
assume A9: S1[p] ; :: thesis: S1[ 'not' p]
thus still_not-bound_in () = still_not-bound_in p by QC_LANG3:7
.= still_not-bound_in ('not' (Al2 -Cast p)) by
.= still_not-bound_in (Al2 -Cast ()) ; :: thesis: verum
end;
A10: for p, q being Element of CQC-WFF Al st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of CQC-WFF Al; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A11: ( S1[p] & S1[q] ) ; :: thesis: S1[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 ;
hence still_not-bound_in (p '&' q) = \/ by
.= still_not-bound_in (Al2 -Cast (p '&' q)) by ;
:: thesis: verum
end;
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st S1[p] holds
S1[ All (x,p)]
proof
let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al st S1[p] holds
S1[ All (x,p)]

let p be Element of CQC-WFF Al; :: thesis: ( S1[p] implies S1[ All (x,p)] )
assume A13: S1[p] ; :: thesis: S1[ 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 ;
then still_not-bound_in (All (x,p)) = \ {x} by
.= still_not-bound_in (Al2 -Cast (All (x,p))) by ;
hence S1[ 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
( S1[ VERUM Al] & S1[P ! l] & ( S1[p] implies S1[ 'not' p] ) & ( S1[p] & S1[q] implies S1[p '&' q] ) & ( S1[p] implies S1[ All (x,p)] ) ) by A1, A2, A8, A10;
for p being Element of CQC-WFF Al holds S1[p] from hence for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p) ; :: thesis: verum