let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A holds still_not-bound_in p is finite
defpred S₁[ Element of QC-WFF A] means still_not-bound_in $1 is finite ;
A1: for p being Element of QC-WFF A holds
( ( p is atomic implies S₁[p] ) & S₁[ VERUM A] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )

proof

let p be Element of QC-WFF A; :: thesis: ( ( p is atomic implies S₁[p] ) & S₁[ VERUM A] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is atomic implies still_not-bound_in p is finite ) :: thesis: ( S₁[ VERUM A] & ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )

proof

deffunc H₅( set ) -> set = (the_arguments_of p) . $1;
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= len (the_arguments_of p) );
defpred S₃[ Nat] means ( 1 <= $1 & $1 <= len (the_arguments_of p) & (the_arguments_of p) . $1 in bound_QC-variables A );
A2: { H₅(k) where k is Nat : S₃[k] } c= { H₅(n) where n is Nat : S₂[n] }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { H₅(k) where k is Nat : S₃[k] } or e in { H₅(n) where n is Nat : S₂[n] } )
assume e in { H₅(k) where k is Nat : S₃[k] } ; :: thesis: e in { H₅(n) where n is Nat : S₂[n] }
then ex k being Nat st
( e = H₅(k) & S₃[k] ) ;
hence e in { H₅(n) where n is Nat : S₂[n] } ; :: thesis: verum

end;

assume p is atomic ; :: thesis: still_not-bound_in p is finite
then still_not-bound_in p = still_not-bound_in (the_arguments_of p) by QC_LANG3:4
.= variables_in ((the_arguments_of p),(bound_QC-variables A)) by QC_LANG3:2
.= { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ;
then still_not-bound_in p c= rng (the_arguments_of p) by A2, Th9;
hence still_not-bound_in p is finite ; :: thesis: verum

end;

thus still_not-bound_in (VERUM A) is finite by QC_LANG3:3; :: thesis: ( ( p is negative & S₁[ the_argument_of p] implies S₁[p] ) & ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is negative & still_not-bound_in (the_argument_of p) is finite implies still_not-bound_in p is finite ) by QC_LANG3:6; :: thesis: ( ( p is conjunctive & S₁[ the_left_argument_of p] & S₁[ the_right_argument_of p] implies S₁[p] ) & ( p is universal & S₁[ the_scope_of p] implies S₁[p] ) )
thus ( p is conjunctive & still_not-bound_in (the_left_argument_of p) is finite & still_not-bound_in (the_right_argument_of p) is finite implies still_not-bound_in p is finite ) :: thesis: ( p is universal & S₁[ the_scope_of p] implies S₁[p] )

proof

assume that
A3: p is conjunctive and
A4: still_not-bound_in (the_left_argument_of p) is finite and
A5: still_not-bound_in (the_right_argument_of p) is finite ; :: thesis: still_not-bound_in p is finite
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) by A3, QC_LANG3:9;
hence still_not-bound_in p is finite by A4, A5; :: thesis: verum

end;

assume that
A6: p is universal and
A7: still_not-bound_in (the_scope_of p) is finite ; :: thesis: S₁[p]
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)} by A6, QC_LANG3:11;
hence S₁[p] by A7; :: thesis: verum

end;

thus for p being Element of QC-WFF A holds S₁[p] from QC_LANG1:sch 2(A1); :: thesis: verum