deffunc H₁( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H₂( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H₃( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H₄( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
reconsider Emp = {} as Subset of (bound_QC-variables A) by XBOOLE_1:2;
consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that
A1: ( F . (VERUM A) = Emp & ( for p being Element of QC-WFF A holds
( ( p is atomic implies F . p = H₄(p) ) & ( p is negative implies F . p = H₃(F . (the_argument_of p)) ) & ( p is conjunctive implies F . p = H₂(F . (the_left_argument_of p),F . (the_right_argument_of p)) ) & ( p is universal implies F . p = H₁(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch 3();
take F . p ; :: thesis: ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( F . p = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((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 ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) )
take F ; :: thesis: ( F . p = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((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 ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) )
thus F . p = F . p ; :: thesis: for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((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 ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
let p be Element of QC-WFF A; :: thesis: ( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((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 ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus F . (VERUM A) = {} by A1; :: thesis: ( ( p is atomic implies F . p = { ((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 ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is atomic implies F . p = { ((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 ) } ) :: thesis: ( ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

proof

assume p is atomic ; :: thesis: F . p = { ((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 F . p = still_not-bound_in (the_arguments_of p) by A1;
hence F . p = { ((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 ) } ; :: thesis: verum

end;

thus ( p is negative implies F . p = F . (the_argument_of p) ) by A1; :: thesis: ( ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A1; :: thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )
assume p is universal ; :: thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}
hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A1; :: thesis: verum